def tw

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

560# halving while both are even: ntw computes 2^c gcd(a, b) (as c doublings)
561def tw(f: Nat, +a: Nat, +b: Nat, +c: Nat, +ha0: {Nat.is_lt(0n, a) == True{} : Bool}, +hb0: {Nat.is_lt(0n, b) == True{} : Bool}, +haf: {Nat.is_lt(a, C.pow2(f)) == True{} : Bool}, +hf: {Nat.is_le(f, 140n) == True{} : Bool}, +hab: {Nat.is_lt(Nat.mul(a, b), C.pow2(139n)) == True{} : Bool}) -> {ntw(f, a, b, c, nev2(a, b)) == ndbl(c, M.gcd(a, b)) : Nat}:
562  match f:
563    case 0n:
564      Empty.absurd({ntw(0n, a, b, c, nev2(a, b)) == ndbl(c, M.gcd(a, b)) : Nat}, pos_absurd1(a, ha0, haf))
565    case 1n+ +g:
566      +hg = N.le_trans(g, 1n+g, 140n, N.le_succ(g), hf)
567      tw_case(g, a, b, c, ha0, hb0, haf, hf, hab, a2 => b2 => c2 => ha2 => hb2 => haf2 => hab2 => tw(g, a2, b2, c2, ha2, hb2, haf2, hg, hab2), nev2(a, b), {==})