decidable lt comparison function

source/arithmetics/naturals.mmt

@@ -78,6 +78,8 @@ theory NaturalArithmetics : base:?Logic =
     lemma_le_pred_le : {x : ℕ , n : ℕ } ⊦ (`?NaturalNumbers?succ : ℕ ⟶ ℕ) x ≤ n ⟶ ⊦ x ≤ n ❘# le_pred_le 3❙
     lemma_zero_le : {n : ℕ} ⊦ 0 ≤ n ❘ # lemma_zero_le 1 ❙
     lemma_zero_succ_lt : {n : ℕ} ⊦ 0 < `?NaturalNumbers?succ  n ❘# lemma_zero_succ_lt 1 ❙
+    lemma_lt_succ_succ : {a : ℕ} {b : ℕ} ⊦  a < b ⟶ ⊦  `?NaturalNumbers?succ a < `?NaturalNumbers?succ b ❘# lemma_lt_succ_succ 1 2 3 ❙
+    lemma_le_succ_succ : {a : ℕ} {b : ℕ} ⊦  a ≤ b ⟶  ⊦ `?NaturalNumbers?succ a ≤ `?NaturalNumbers?succ b ❘ # lemma_le_succ_succ 1 2 3 ❙
 
 
     // added by sw ❙
@@ -178,9 +180,12 @@ theory CompDec : base:?Logic =
     include ?NaturalArithmetics ❙
     include lfxcop:?LFCoprod❙
 
+    le_dec_add : {a : ℕ} {b : ℕ} ((⊦ a ≤ b) ⨁ (⊦ b < a)) ⟶ ((⊦ `?NaturalNumbers?succ a ≤ `?NaturalNumbers?succ b) ⨁ (⊦ `?NaturalNumbers?succ b < `?NaturalNumbers?succ a)) ❙
+    le_dec_add_l : {a : ℕ} {b : ℕ } {h : ⊦ a ≤ b} ⊦ le_dec_add a b (h ↪l (⊦ b < a)) ≐ ((lemma_le_succ_succ a b h ) ↪l (⊦ `?NaturalNumbers?succ b < `?NaturalNumbers?succ a)) ❙
+    le_dec_add_r : {a : ℕ} {b : ℕ } {h : ⊦ b < a} ⊦ le_dec_add a b ((⊦ a ≤ b) r↩ h) ≐ ( (⊦ `?NaturalNumbers?succ a ≤ `?NaturalNumbers?succ b) r↩ (lemma_lt_succ_succ b a  h)) ❙
 
     le_dec : {a : ℕ} {b : ℕ} ((⊦ a ≤ b) ⨁ (⊦ b < a)) ❙
     le_dec_b : {n : ℕ} ⊦ le_dec 0 n ≐  ((lemma_zero_le n) ↪l (⊦ n < 0)) ❙
     le_dec_b2 : {n : ℕ}  ⊦ le_dec (`?NaturalNumbers?succ n) 0 ≐  ((⊦ (`?NaturalNumbers?succ n) ≤ 0 ) r↩ (lemma_zero_succ_lt n)) ❙
-    le_dec_S : {n : ℕ} {m : ℕ} ⊦ le_dec (`?NaturalNumbers?succ n) (`?NaturalNumbers?succ m) ≐ le_dec n m  ❙
+    le_dec_S : {n : ℕ} {m : ℕ} ⊦ le_dec (`?NaturalNumbers?succ n) (`?NaturalNumbers?succ m) ≐ le_dec_add n m (le_dec n m)  ❙
 ❚
\ No newline at end of file