IntegerGCDStarter

Absolute values, divisibility, GCD, and Bézout over all quotient integers

Open in Workbench View on GitHub

1-- Absolute values, divisibility, GCD, and Bézout over all quotient integers2-- 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 IntegerGCDStarter9import Grace.Cumulus.NumberTheory1011theorem all_integer_inputs (x y : Integer)12  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧ u * x + v * y = integerOfNat(integerGCD(x, y))13proof14  exact integerGCD.bezout at x, y with *1516theorem canonical_gcd (x y : Integer)17  shows IsIntegerGCD(x, y, integerGCD(x, y))18proof19  exact integerGCD.correct at x, y with *2021theorem negative_gcd22  shows integerGCD(integerNegativeOfNat(252), integerOfNat(198)) = 1823proof24  simp [integerGCD, integerNatAbs.ofNegativeNat, integerNatAbs.ofNat]2526theorem absolute_product (x y : Integer)27  shows integerNatAbs(x * y) = integerNatAbs(x) * integerNatAbs(y)28proof29  exact integerNatAbs.mul at x, y with *3031-- (-4)*(-252) + (-5)*198 = 18, an equality in the quotient integers.32theorem signed_identity33  shows integerNegativeOfNat(4) * integerNegativeOfNat(252) + integerNegativeOfNat(5) * integerOfNat(198) = integerOfNat(18)34proof35  simp [integerMulValue.negative_negative, integerMulValue.negative_ofNat]36  simp [integerOfNat, integerNegativeOfNat, integerAddValue.classes, integerClassSum]37  apply integerClass.eq with *{4}38  compute39