BezoutStarter

Signed Bézout identities, proved over quotient integers

Open in Workbench View on GitHub

1-- Signed Bézout identities, proved over 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 BezoutStarter9import Grace.Cumulus.NumberTheory1011-- Every natural-input GCD has coefficients in the existing integer carrier.12theorem bezout (a b : Nat)13  shows ∃ u, Integer(u) ∧ ∃ v, Integer(v) ∧14    integerLinearCombination(u, v, a, b) = integerOfNat(gcd(a, b))15proof16  exact gcd.bezout at a, b with *1718-- 1*54 + (-2)*24 = 6. The equality is between quotient integers.19theorem signed_example20  shows integerLinearCombination(integerOfNat(1), integerNegativeOfNat(2), 54, 24) = integerOfNat(gcd(54, 24))21proof22  have result : gcd(54, 24) = 623  . compute24  rw result25  simp [integerOfNat, integerNegativeOfNat, integerLinearCombination.classes]26  apply integerClass.eq with *{4}27  compute2829-- Ordinary signed arithmetic has familiar notation and reusable laws.30theorem cancel (x : Integer)31  shows x + (-x) = integerZero32proof33  exact integerAddValue.neg_right at x with *3435theorem distribute (x y z : Integer)36  shows x * (y + z) = x * y + x * z37proof38  exact integerMulValue.distribute_right at x, y, z with *39