def xg_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mexp.bend:45

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
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/f64cmp.bend as FC

45def xg_c(+E: Nat, +c: Bool, +hc: {Nat.is_eq(E, 0n) == c : Bool}) -> {Nat.is_le(1926n, SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n))) == True{} : Bool}:
46  match c:
47    case True{}:
48      {==}
49    case False{}:
50      L.subst(Nat, z => {Nat.is_le(1926n, z) == True{} : Bool}, Nat.add(1925n, E), Nat.sub(Nat.add(E, SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E)), e_ge1(E, hc))