def unique

stelliferous@0.0.2.0 · proofs/nat_division.bend:114

import Base

114def unique(+a: Nat,+b: Nat,+q: Nat,+r: Nat,e: {a == Nat.add(Nat.mul(q,b),r) : Nat},positive: {Nat.is_lt(0n,b) == True{} : Bool},
115  bounded: {Nat.is_lt(r,b) == True{} : Bool}) -> {Nat.divmod(a,b) == (q,r) : Nat & Nat}:
116  %Equal.sym(Nat,a,Nat.add(Nat.mul(q,b),r),e) : {Nat.divmod(_,b) == (q,r) : Nat & Nat}
117  quotient_remainder(q,r,b,positive,bounded)