def wstep

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

import Base

50# from n == l g and a mod n == r g: a == (q l + r) g and n == l g
51def wstep(+q: Nat, w: Wit) -> Wit:
52  match w:
53    case W{+l, r}:
54      W{Nat.add(Nat.mul(q, l), r), l}