def xem_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:72

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

72def xem_c(+e: Nat, +z: Bool, +hz: {Nat.is_eq(e, 0n) == z : Bool}) -> {Nat.add(1926n, Nat.sub(e, 1n)) == AG.xe(e) : Nat}:
73  match z:
74    case True{}:
75      +e0 = N.eq_from_is_eq(e, 0n, hz)
76      L.subst(Nat, w => {Nat.add(1926n, Nat.sub(w, 1n)) == AG.xe(w) : Nat}, 0n, e, Equal.sym(Nat, e, 0n, e0), {==})
77    case False{}:
78      +e1 = Equal.cong(Nat, Nat, w => Nat.add(1925n, w), Nat.add(1n, Nat.sub(e, 1n)), e, N.sub_add(e, 1n, nz_le(e, hz)))
79      Equal.trans(Nat, Nat.add(1926n, Nat.sub(e, 1n)), Nat.add(1925n, e), AG.xe(e), e1, Equal.sym(Nat, AG.xe(e), Nat.add(1925n, e), AG.xe_n(e, hz)))