def lt_succ_le

stelliferous@0.0.2.0 · proofs/nat_division.bend:13

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

13def lt_succ_le(+n: Nat,+m: Nat,h: {Nat.is_lt(n,1n+m) == True{} : Bool}) -> {Nat.is_le(n,m) == True{} : Bool}:
14  match n m:
15    case 0n 0n:
16      {==}
17    case 0n 1n+m:
18      {==}
19    case 1n+ +n 0n:
20      Empty.absurd({Nat.is_le(1n+n,0n) == True{} : Bool},WordEncoding.false_true(Equal.trans(Bool,False{},Nat.is_lt(n,0n),True{},Equal.sym(Bool,
21              Nat.is_lt(n,0n),False{},lt_zero(n)),h)))
22    case 1n+n 1n+m:
23      lt_succ_le(n,m,h)