def internal_fin_wrap

bend-mathlib@0.8.1.0 · u32.bend:280

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

280def internal_fin_wrap(+e: Nat, -s: Nat, +m: Nat, o: Bool, eq: {Nat.add(e, Bool.pick(Nat, o, m, 0n)) == s : Nat}, h: MNat.lt(e, m)) -> {e == Nat.mod(s, m) : Nat}:
281  match o:
282    case False{}:
283      %eq : {e == Nat.mod(_, m) : Nat}
284      %MNat.add_zero_sym(e) : {e == Nat.mod(_, m) : Nat}
285      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))
286    case True{}:
287      %eq : {e == Nat.mod(_, m) : Nat}
288      %MNat.add_comm(m, e) : {e == Nat.mod(_, m) : Nat}
289      %MNat.add_mod_left_sym(e, m) : {e == _ : Nat}
290      Equal.sym(Nat, Nat.mod(e, m), e, MNat.mod_eq_of_lt(e, m, h))