Skip to main content

axiom/NatOrder

Reference for mo:core/axiom/NatOrder 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/NatOrder

Status​

  • Spec-only axiom module

Public API​

Types​

  • Nat

Lemmas​

leAntisym(a : Nat, b : Nat) : ()​

Establishes a == b in the current proof context.

Contract

requires a <= b;
requires b <= a;
ensures a == b;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leTrans(a : Nat, b : Nat, c : Nat) : ()​

Establishes a <= c in the current proof context.

Contract

requires a <= b;
requires b <= c;
ensures a <= c;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leTotal(a : Nat, b : Nat) : ()​

Establishes a <= b or b <= a in the current proof context.

Contract

ensures a <= b or b <= a;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

ltStep(a : Nat, b : Nat) : ()​

Establishes (a < b) <==> (a + 1 <= b) in the current proof context.

Contract

ensures (a < b) <==> (a + 1 <= b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

leCancelAdd(a : Nat, b : Nat, k : Nat) : ()​

Establishes (a + k <= b + k) <==> (a <= b) in the current proof context.

Contract

ensures (a + k <= b + k) <==> (a <= b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

ltCancelAdd(a : Nat, b : Nat, k : Nat) : ()​

Establishes (a + k < b + k) <==> (a < b) in the current proof context.

Contract

ensures (a + k < b + k) <==> (a < b);

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

zeroLe(a : Nat) : ()​

Establishes 0 <= a in the current proof context.

Contract

ensures 0 <= a;

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/NatOrder.
  • Exposes 7 trusted lemmas.