def e_ge1

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

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/math/typed/u32laws.bend as LW

38def e_ge1(+E: Nat, +h: {Nat.is_eq(E, 0n) == False{} : Bool}) -> {Nat.is_le(1926n, Nat.add(1925n, E)) == True{} : Bool}:
39  match E:
40    case 0n:
41      Empty.absurd({Nat.is_le(1926n, Nat.add(1925n, 0n)) == True{} : Bool}, LW.true_ne_false(h))
42    case 1n+ +p:
43      N.zero_le(p)