def internal_div_unique

bend-mathlib@0.8.1.0 · u32.bend:913

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

913def internal_div_unique(+q: Nat, b: Nat, +r: Nat, -a: Nat, hb: MNat.lt(0n, b), e: {Nat.add(Nat.mul(q, b), r) == a : Nat}, h: MNat.lt(r, b)) -> {q == Nat.div(a, b) : Nat}:
914  match b:
915    case 0n:
916      Empty.absurd({q == Nat.div(a, 0n) : Nat}, MNat.internal_false_ne_true(hb))
917    case 1n++bp:
918      %e : {q == Nat.div(_, 1n+bp) : Nat}
919      %MNat.add_comm(r, Nat.mul(q, 1n+bp)) : {q == Nat.div(_, 1n+bp) : Nat}
920      %MNat.add_mul_div_right_sym(r, q, bp) : {q == _ : Nat}
921      %Equal.sym(Nat, Nat.div(r, 1n+bp), 0n, MNat.div_eq_zero_of_le(r, bp, MNat.le_of_lt_succ(r, bp, h))) : {q == Nat.add(_, q) : Nat}
922      {==}