def gcd_odd2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/bgcdnat.bend:160

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M

160# a odd: gcd(a, 2 m) = gcd(a, m)
161def gcd_odd2(+a: Nat, +ha: {Nat.mod(a, 2n) == 1n : Nat}, +m: Nat) -> {M.gcd(a, Nat.double(m)) == M.gcd(a, m) : Nat}:
162  gcd_eq(a, Nat.double(m), a, m, d => ka => kb => ea => eb => odd2_t1_at(a, ha, m, d, ka, kb, ea, eb), d => ka => km => ea => em => odd2_t2_at(a, m, d, ka, km, ea, em))