def div_of

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:81

import Base

81def div_of(-t: Nat, +size: Nat, +q: Nat, +r: Nat, below: {Nat.is_lt(r, size) == True{} : Bool},
82  sum: {Nat.add(Nat.mul(q, size), r) == t : Nat}) -> {Nat.div(t, size) == q : Nat}:
83  Equal.sym(Nat, q, Nat.div(t, size),
84    Equal.cong(Nat & Nat, Nat, pair => Pair.fst(Nat, Nat, pair), (q, r), Nat.divmod(t, size), split_divmod(t, size, q, r, below, sum)))