def divides

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:252

import Base
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as NatProofs

252# q * (1 + rest) = count gives count divmod (1 + rest) = (q, 0).
253def divides(+count: Nat, +rest: Nat, +quotient: Nat, exact: {Nat.mul(quotient, 1n+rest) == count : Nat}) ->
254  {Nat.divmod(count, 1n+rest) == (quotient, 0n) : Nat & Nat}:
255  Equal.trans(Nat & Nat, Nat.divmod(count, 1n+rest), Nat.divmod(Nat.add(Nat.mul(quotient, 1n+rest), 0n), 1n+rest), (quotient, 0n),
256    Equal.cong(Nat, Nat & Nat, x => Nat.divmod(x, 1n+rest), count, Nat.add(Nat.mul(quotient, 1n+rest), 0n),
257      Equal.sym(Nat, Nat.add(Nat.mul(quotient, 1n+rest), 0n), count,
258        Equal.trans(Nat, Nat.add(Nat.mul(quotient, 1n+rest), 0n), Nat.mul(quotient, 1n+rest), count,
259          add_zero_right(Nat.mul(quotient, 1n+rest)), exact))),
260    Equal.sym(Nat & Nat, (quotient, 0n), Nat.divmod(Nat.add(Nat.mul(quotient, 1n+rest), 0n), 1n+rest),
261      NatProofs.divmod_exact(quotient, 1n+rest, 0n, Unit{})))