def bumped_quotient

stelliferous@0.0.2.0 · proofs/nat_division.bend:50

import Base

50def bumped_quotient(pair: Nat & Nat) -> {Pair.fst(Nat,Nat,bump(pair)) == 1n+Pair.fst(Nat,Nat,pair) : Nat}:
51  (quotient,remainder) = pair
52  {==}