Skip to main content

axiom/DivAddBoundsNat

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Nat

Lemmas​

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.

divAddMonoLeft(a : Nat, a2 : Nat, b : Nat, c : Nat) : ()​

Establishes (a + b) / c <= (a2 + b) / c in the current proof context.

Contract

requires c > 0;
requires a <= a2;
ensures (a + b) / c <= (a2 + b) / c;

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

divAddZeroRight(a : Nat, c : Nat) : ()​

Establishes (a + 0) / c == a / c in the current proof context.

Contract

requires c > 0;
ensures (a + 0) / c == a / c;

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