Skip to main content

axiom/DivAddBoundsInt

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

Status​

  • Spec-only axiom module

Public API​

Types​

  • Int

Lemmas​

divAddLowerPos(a : Int, b : Int, c : Int) : ()​

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

Contract

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

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

divAddUpperPos(a : Int, b : Int, c : Int) : ()​

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.

divAddMonoLeftPos(a : Int, a2 : Int, b : Int, c : Int) : ()​

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.

divAddZeroRightPos(a : Int, c : Int) : ()​

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