~/jendhub

def internal_mod_eq_of_wit

bend-mathlib@0.8.1.0 · nat.bend:1996

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

1996def internal_mod_eq_of_wit(+a: Nat, +b: Nat, w: &k:Nat -> {Nat.add(a, k) == b : Nat}) -> {Nat.mod(a, 1n+b) == a : Nat}:
1997  match w:
1998    case (+k, e):
1999      %e : {Nat.mod(a, 1n+_) == a : Nat}
2000      Equal.trans(Nat, Nat.mod(a, 1n+Nat.add(a, k)), Nat.add(a, 0n), a, internal_mod_go_small(a, k, 0n, 0n), add_zero(a))

Uses (8)

Used by (1)