def gcd_both

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/gcd.bend:75

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as R

75def gcd_both(fuel: Nat, +a: Nat, +b: Nat, +hb: {Nat.is_le(b, fuel) == True{} : Bool}) -> divides_both(a, b, M.gcd_go(fuel, a, b), ws(fuel, a, b)):
76  match fuel b:
77    case 0n 0n:
78      (Equal.sym(Nat, Nat.add(a, 0n), a, A.add_zero(a)), {==})
79    case 0n 1n+bp:
80      Empty.absurd(divides_both(a, 1n+bp, M.gcd_go(0n, a, 1n+bp), ws(0n, a, 1n+bp)), L.false_true(hb))
81    case 1n+f 0n:
82      (Equal.sym(Nat, Nat.add(a, 0n), a, A.add_zero(a)), {==})
83    case 1n+ +f 1n+ +bp:
84      step_both(bp, a, M.gcd_go(f, 1n+bp, Nat.mod(a, 1n+bp)), ws(f, 1n+bp, Nat.mod(a, 1n+bp)), gcd_both(f, 1n+bp, Nat.mod(a, 1n+bp), N.le_trans(Nat.mod(a, 1n+bp), bp, f, N.lt_succ_le(Nat.mod(a, 1n+bp), bp, R.dm_lt(bp, a)), hb)))