naxiom decompose1: ¬(lt O O).
naxiom decompose2: ∀n. ¬(lt (S n) O).
-ndefinition ltb: ∀n,m:nat. lt n m ∨ ¬(lt n m).
+ndefinition ltb: nat → nat → bool.
#n; nelim n
[ #m; ncases m
- [ napply or_intror; #H; napply (decompose1 H)
- | #m'; napply or_introl; napply lt_O_Sn ]
+ [ napply false
+ | #m'; napply true ]
##| #n'; #Hn'; #m; ncases m
- [ napply or_intror; #H; napply (decompose2 … H)
+ [ napply false
| #m'; ncases (Hn' m')
- [ #H; napply or_introl; napply le_S_S; napply H
- | #H; napply or_intror; #K; napply H; napply le_S_S_to_le; napply K]##]
+ [ napply true
+ | napply false]##]
nqed.