def branch

stelliferous@0.0.2.0 · proofs/binary_division.bend:27

import Base

27def branch(g: Bool,+q: Nat,s: Nat,b: Nat) -> Quotient:
28  match g:
29    case False{}:
30      Quotient{q,s}
31    case True{}:
32      Quotient{1n+q,Nat.sub(s,b)}