def xe_le_c

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

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/f64addg.bend as AG

58def xe_le_c(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(a, 0n) == z : Bool}) -> {Nat.is_le(AG.xe(a), AG.xe(b)) == True{} : Bool}:
59  match z:
60    case True{}:
61      +hb = N.le_trans(1n, 1n+a, b, N.zero_le(a), N.lt_succ_le_succ(a, b, h))
62      +xb = AG.xe_n(b, AG.posz(b, hb))
63      le_rw(AG.xe(a), 1926n, AG.xe_z(a, hz), AG.xe(b), Nat.add(1925n, b), xb, N.le_add_left(1n, b, 1925n, hb))
64    case False{}:
65      +hb = N.le_trans(1n, 1n+a, b, N.zero_le(a), N.lt_succ_le_succ(a, b, h))
66      +xb = AG.xe_n(b, AG.posz(b, hb))
67      le_rw(AG.xe(a), Nat.add(1925n, a), AG.xe_n(a, hz), AG.xe(b), Nat.add(1925n, b), xb, N.le_add_left(a, b, 1925n, N.lt_le(a, b, h)))