DivisionStarter

Executable division and the signed Euclidean coefficient update

Open in Workbench View on GitHub

1-- Executable division and the signed Euclidean coefficient update2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67-- Copyright (c) 2026 Grant Passmore. Apache License 2.0.8module DivisionStarter9import Grace.Cumulus.NumberTheory1011theorem division (n d : Nat)12  requires nonzero : d ≠ 013  shows Nat(quotientNat(n, d)) ∧ n = d * quotientNat(n, d) + n % d ∧ n % d < d14proof15  exact quotientNat.division at n, d with *1617theorem quotient_sample18  shows quotientNat(1234, 37) = 3319proof20  compute2122theorem remainder_sample23  shows 1234 % 37 = 1324proof25  compute2627theorem zero_divisor (n : Nat)28  shows quotientNat(n, 0) = 029proof30  exact quotientNat.zero_right at n with *3132theorem coefficient_step (u v : Integer, a b : Nat)33  shows integerLinearCombination(v, u + (-(integerOfNat(quotientNat(a, b)) * v)), a, b) =34    integerLinearCombination(u, v, b, a % b)35proof36  exact integerLinearCombination.remainder_step at u, v, a, b with *37