axiom/Nat
Reference for mo:core/axiom/Nat in the core library.
This page lists trusted proof lemmas. Calling one adds its ensures facts after its requires clauses are proven; the lemma body itself is part of the trusted base, not a verifier-checked derivation. Use these when ordinary SMT arithmetic needs a precise algebraic step.
Import
mo:core/axiom/Nat
Status
- Spec-only axiom module
Public API
Types
Nat
Lemmas
addZeroRight(a : Nat) : ()
Establishes a + 0 == a in the current proof context.
Contract
ensures a + 0 == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addZeroLeft(a : Nat) : ()
Establishes 0 + a == a in the current proof context.
Contract
ensures 0 + a == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addComm(a : Nat, b : Nat) : ()
Establishes a + b == b + a in the current proof context.
Contract
ensures a + b == b + a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addAssoc(a : Nat, b : Nat, c : Nat) : ()
Establishes (a + b) + c == a + (b + c) in the current proof context.
Contract
ensures (a + b) + c == a + (b + c);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addLeMonoRight(a : Nat, b : Nat, c : Nat) : ()
Establishes a + c <= b + c in the current proof context.
Contract
requires a <= b;
ensures a + c <= b + c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addLeMonoLeft(a : Nat, b : Nat, c : Nat) : ()
Establishes c + a <= c + b in the current proof context.
Contract
requires a <= b;
ensures c + a <= c + b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addLtMonoRight(a : Nat, b : Nat, c : Nat) : ()
Establishes a + c < b + c in the current proof context.
Contract
requires a < b;
ensures a + c < b + c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addLtMonoLeft(a : Nat, b : Nat, c : Nat) : ()
Establishes c + a < c + b in the current proof context.
Contract
requires a < b;
ensures c + a < c + b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addCancelRightEq(a : Nat, b : Nat, c : Nat) : ()
Establishes a == b in the current proof context.
Contract
requires a + c == b + c;
ensures a == b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addCancelLeftEq(a : Nat, b : Nat, c : Nat) : ()
Establishes a == b in the current proof context.
Contract
requires c + a == c + b;
ensures a == b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addCancelRightLe(a : Nat, b : Nat, c : Nat) : ()
Establishes a <= b in the current proof context.
Contract
requires a + c <= b + c;
ensures a <= b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
addCancelLeftLe(a : Nat, b : Nat, c : Nat) : ()
Establishes a <= b in the current proof context.
Contract
requires c + a <= c + b;
ensures a <= b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
leAddRight(a : Nat, b : Nat) : ()
Establishes a <= a + b in the current proof context.
Contract
ensures a <= a + b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
leAddLeft(a : Nat, b : Nat) : ()
Establishes a <= b + a in the current proof context.
Contract
ensures a <= b + a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
ltAddRight(a : Nat, b : Nat) : ()
Establishes a < a + b in the current proof context.
Contract
requires b > 0;
ensures a < a + b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulZeroRight(a : Nat) : ()
Establishes a * 0 == 0 in the current proof context.
Contract
ensures a * 0 == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulZeroLeft(a : Nat) : ()
Establishes 0 * a == 0 in the current proof context.
Contract
ensures 0 * a == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulOneRight(a : Nat) : ()
Establishes a * 1 == a in the current proof context.
Contract
ensures a * 1 == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulOneLeft(a : Nat) : ()
Establishes 1 * a == a in the current proof context.
Contract
ensures 1 * a == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulComm(a : Nat, b : Nat) : ()
Establishes a * b == b * a in the current proof context.
Contract
ensures a * b == b * a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulAssoc(a : Nat, b : Nat, c : Nat) : ()
Establishes (a * b) * c == a * (b * c) in the current proof context.
Contract
ensures (a * b) * c == a * (b * c);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulLeMonoRight(a : Nat, b : Nat, c : Nat) : ()
Establishes a * c <= b * c in the current proof context.
Contract
requires a <= b;
ensures a * c <= b * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulLeMonoLeft(a : Nat, b : Nat, c : Nat) : ()
Establishes c * a <= c * b in the current proof context.
Contract
requires a <= b;
ensures c * a <= c * b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulLtMonoRight(a : Nat, b : Nat, c : Nat) : ()
Establishes a * c < b * c in the current proof context.
Contract
requires a < b;
requires c > 0;
ensures a * c < b * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulLtMonoLeft(a : Nat, b : Nat, c : Nat) : ()
Establishes c * a < c * b in the current proof context.
Contract
requires a < b;
requires c > 0;
ensures c * a < c * b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulCancelRightEq(a : Nat, b : Nat, c : Nat) : ()
Establishes a == b in the current proof context.
Contract
requires c > 0;
requires a * c == b * c;
ensures a == b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulCancelLeftEq(a : Nat, b : Nat, c : Nat) : ()
Establishes a == b in the current proof context.
Contract
requires c > 0;
requires c * a == c * b;
ensures a == b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulCancelRightLe(a : Nat, b : Nat, c : Nat) : ()
Establishes a <= b in the current proof context.
Contract
requires c > 0;
requires a * c <= b * c;
ensures a <= b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulCancelLeftLe(a : Nat, b : Nat, c : Nat) : ()
Establishes a <= b in the current proof context.
Contract
requires c > 0;
requires c * a <= c * b;
ensures a <= b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulPos(a : Nat, b : Nat) : ()
Establishes a * b > 0 in the current proof context.
Contract
requires a > 0;
requires b > 0;
ensures a * b > 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
leMulRight(a : Nat, b : Nat) : ()
Establishes a <= a * b in the current proof context.
Contract
requires b > 0;
ensures a <= a * b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
leMulLeft(a : Nat, b : Nat) : ()
Establishes b <= a * b in the current proof context.
Contract
requires a > 0;
ensures b <= a * b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divZero(c : Nat) : ()
Establishes 0 / c == 0 in the current proof context.
Contract
requires c > 0;
ensures 0 / c == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divOne(a : Nat) : ()
Establishes a / 1 == a in the current proof context.
Contract
ensures a / 1 == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divLeSelf(a : Nat, c : Nat) : ()
Establishes a / c <= a in the current proof context.
Contract
requires c > 0;
ensures a / c <= a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divByLargerZero(a : Nat, c : Nat) : ()
Establishes a / c == 0 in the current proof context.
Contract
requires c > 0;
requires a < c;
ensures a / c == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulLeSelf(a : Nat, c : Nat) : ()
Establishes (a / c) * c <= a in the current proof context.
Contract
requires c > 0;
ensures (a / c) * c <= a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulLtSelf(a : Nat, c : Nat) : ()
Establishes a < ((a / c) + 1) * c in the current proof context.
Contract
requires c > 0;
ensures a < ((a / c) + 1) * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divLeMonoNum(a : Nat, b : Nat, c : Nat) : ()
Establishes a / c <= b / c in the current proof context.
Contract
requires c > 0;
requires a <= b;
ensures a / c <= b / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divLeMonoDenom(a : Nat, c : Nat, d : Nat) : ()
Establishes a / d <= a / c in the current proof context.
Contract
requires c > 0;
requires d > 0;
requires c <= d;
ensures a / d <= a / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivCancelRight(a : Nat, c : Nat) : ()
Establishes (a * c) / c == a in the current proof context.
Contract
requires c > 0;
ensures (a * c) / c == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivCancelLeft(a : Nat, c : Nat) : ()
Establishes (c * a) / c == a in the current proof context.
Contract
requires c > 0;
ensures (c * a) / c == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivCancel(a : Nat, b : Nat) : ()
Establishes (a * b) / b == a in the current proof context.
Contract
requires b > 0;
ensures (a * b) / b == a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivCancelOther(a : Nat, b : Nat) : ()
Establishes (a * b) / a == b in the current proof context.
Contract
requires a > 0;
ensures (a * b) / a == b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divEqFromRange(a : Nat, q : Nat, c : Nat) : ()
Establishes a / c == q in the current proof context.
Contract
requires c > 0;
requires q * c <= a;
requires a < (q + 1) * c;
ensures a / c == q;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divRangeFromEq(a : Nat, q : Nat, c : Nat) : ()
Establishes the listed proof facts in the current verification context.
Contract
requires c > 0;
requires a / c == q;
ensures q * c <= a;
ensures a < (q + 1) * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divLtOfLtMul(a : Nat, b : Nat, c : Nat) : ()
Establishes a / c < b in the current proof context.
Contract
requires c > 0;
requires a < b * c;
ensures a / c < b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divLeOfLeMul(a : Nat, b : Nat, c : Nat) : ()
Establishes a / c <= b in the current proof context.
Contract
requires c > 0;
requires a <= b * c;
ensures a / c <= b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divGeOfGeMul(a : Nat, b : Nat, c : Nat) : ()
Establishes b <= a / c in the current proof context.
Contract
requires c > 0;
requires b * c <= a;
ensures b <= a / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
ltMulOfDivLt(a : Nat, b : Nat, c : Nat) : ()
Establishes a < b * c in the current proof context.
Contract
requires c > 0;
requires a / c < b;
ensures a < b * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
ltMulOfDivLe(a : Nat, b : Nat, c : Nat) : ()
Establishes a < (b + 1) * c in the current proof context.
Contract
requires c > 0;
requires a / c <= b;
ensures a < (b + 1) * c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
leMulOfDivGe(a : Nat, b : Nat, c : Nat) : ()
Establishes b * c <= a in the current proof context.
Contract
requires c > 0;
requires b <= a / c;
ensures b * c <= a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divAddLower(a : Nat, b : Nat, c : Nat) : ()
Establishes a / c + b / c <= (a + b) / c in the current proof context.
Contract
requires c > 0;
ensures a / c + b / c <= (a + b) / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divAddUpper(a : Nat, b : Nat, c : Nat) : ()
Establishes (a + b) / c <= a / c + b / c + 1 in the current proof context.
Contract
requires c > 0;
ensures (a + b) / c <= a / c + b / c + 1;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divAddMulExact(a : Nat, k : Nat, c : Nat) : ()
Establishes (a + k * c) / c == (a / c) + k in the current proof context.
Contract
requires c > 0;
ensures (a + k * c) / c == (a / c) + k;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulLe(a : Nat, b : Nat, c : Nat) : ()
Establishes (((a * b) / c) * c) <= (a * b) in the current proof context.
Contract
requires c > 0;
ensures (((a * b) / c) * c) <= (a * b);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivLe(a : Nat, b : Nat, c : Nat) : ()
Establishes ((a * b) / c) <= a in the current proof context.
Contract
requires c > 0;
requires b <= c;
ensures ((a * b) / c) <= a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivLt(a : Nat, b : Nat, c : Nat) : ()
Establishes ((a * b) / c) < a in the current proof context.
Contract
requires c > 0;
requires b < c;
requires a > 0;
ensures ((a * b) / c) < a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivGe(a : Nat, b : Nat, c : Nat) : ()
Establishes a <= ((a * b) / c) in the current proof context.
Contract
requires c > 0;
requires c <= b;
ensures a <= ((a * b) / c);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulLower(a : Nat, b : Nat, c : Nat) : ()
Establishes (a / c) * b <= (a * b) / c in the current proof context.
Contract
requires c > 0;
ensures (a / c) * b <= (a * b) / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
mulDivLower(a : Nat, b : Nat, c : Nat) : ()
Establishes a * (b / c) <= (a * b) / c in the current proof context.
Contract
requires c > 0;
ensures a * (b / c) <= (a * b) / c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulUpperLeft(a : Nat, b : Nat, c : Nat) : ()
Establishes (a * b) / c <= ((a / c) + 1) * b in the current proof context.
Contract
requires c > 0;
ensures (a * b) / c <= ((a / c) + 1) * b;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divMulUpperRight(a : Nat, b : Nat, c : Nat) : ()
Establishes (a * b) / c <= ((b / c) + 1) * a in the current proof context.
Contract
requires c > 0;
ensures (a * b) / c <= ((b / c) + 1) * a;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
modBounds(a : Nat, c : Nat) : ()
Establishes a % c < c in the current proof context.
Contract
requires c > 0;
ensures a % c < c;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
divModDecomp(a : Nat, c : Nat) : ()
Establishes a == (a / c) * c + (a % c) in the current proof context.
Contract
requires c > 0;
ensures a == (a / c) * c + (a % c);
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
modMulZero(a : Nat, c : Nat) : ()
Establishes (a * c) % c == 0 in the current proof context.
Contract
requires c > 0;
ensures (a * c) % c == 0;
Use when: a proof needs this fact explicitly and the solver has not derived it automatically.
Summary
- Spec-only axiom module under
mo:core/axiom/Nat. - Exposes 66 trusted lemmas.