def xe_le

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

69def xe_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(AG.xe(a), AG.xe(b)) == True{} : Bool}:
70  xe_le_c(a, b, h, Nat.is_eq(a, 0n), {==})