def mod_of

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

import Base

86def mod_of(-t: Nat, +size: Nat, +q: Nat, +r: Nat, below: {Nat.is_lt(r, size) == True{} : Bool},
87  sum: {Nat.add(Nat.mul(q, size), r) == t : Nat}) -> {Nat.mod(t, size) == r : Nat}:
88  Equal.sym(Nat, r, Nat.mod(t, size),
89    Equal.cong(Nat & Nat, Nat, pair => Pair.snd(Nat, Nat, pair), (q, r), Nat.divmod(t, size), split_divmod(t, size, q, r, below, sum)))