def lt_ne

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/f64bits.bend:170

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

170def lt_ne(+a: Nat, +m: Nat, +h: {Nat.is_lt(a, 1n+m) == True{} : Bool}) -> {Nat.is_lt(a, m) == Bool.not(Nat.is_eq(a, m)) : Bool}:
171  match a m:
172    case 0n 0n:
173      {==}
174    case 0n 1n+ +mp:
175      {==}
176    case 1n+ +ap 0n:
177      Empty.absurd({Nat.is_lt(1n+ap, 0n) == Bool.not(Nat.is_eq(1n+ap, 0n)) : Bool}, N.lt_zero_absurd(ap, h))
178    case 1n+ +ap 1n+ +mp:
179      lt_ne(ap, mp, h)