propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / rtmap_sor.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma
index 0b3f0ddaa59d345586212b12658283e426aff7f2..bcc7055219a858e6c0b5cf6364fe3874744a47a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/rtmap_sor.ma
@@ -12,8 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/xoa/or_3.ma".
+include "ground/xoa/ex_3_1.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/notation/relations/runion_3.ma".
+include "ground/arith/nat_plus.ma".
+include "ground/arith/nat_le_max.ma".
 include "ground/relocation/rtmap_isfin.ma".
 include "ground/relocation/rtmap_sle.ma".
 
@@ -305,7 +309,8 @@ qed-.
 
 lemma sor_tls: ∀f1,f2,f. f1 ⋓ f2 ≘ f →
                ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≘ ⫱*[n]f.
-#f1 #f2 #f #Hf #n elim n -n /2 width=1 by sor_tl/
+#f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
+/2 width=1 by sor_tl/
 qed.
 
 (* Properies with test for identity *****************************************)
@@ -370,11 +375,11 @@ lemma sor_fcla_ex: ∀f1,n1. 𝐂❪f1❫ ≘ n1 → ∀f2,n2. 𝐂❪f2❫ ≘
                    ∃∃f,n. f1 ⋓ f2 ≘ f & 𝐂❪f❫ ≘ n & (n1 ∨ n2) ≤ n & n ≤ n1 + n2.
 #f1 #n1 #Hf1 elim Hf1 -f1 -n1 /3 width=6 by sor_isid_sn, ex4_2_intro/
 #f1 #n1 #Hf1 #IH #f2 #n2 * -f2 -n2 /3 width=6 by fcla_push, fcla_next, ex4_2_intro, sor_isid_dx/
-#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <plus_n_Sm ] (**) (* full auto fails *)
-[ /3 width=7 by fcla_next, sor_pn, max_S2_le_S, le_S_S, ex4_2_intro/
-| /4 width=7 by fcla_next, sor_nn, le_S, le_S_S, ex4_2_intro/
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
+[ /3 width=7 by fcla_next, sor_pn, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
+| /4 width=7 by fcla_next, sor_nn, nle_succ_dx, nle_succ_bi, ex4_2_intro/
 | /3 width=7 by fcla_push, sor_pp, ex4_2_intro/
-| /3 width=7 by fcla_next, sor_np, max_S1_le_S, le_S_S, ex4_2_intro/
+| /3 width=7 by fcla_next, sor_np, nle_max_sn_succ_sn, nle_succ_bi, ex4_2_intro/
 ]
 qed-.
 
@@ -395,7 +400,7 @@ lemma sor_fwd_fcla_sn_ex: ∀f,n. 𝐂❪f❫ ≘ n → ∀f1,f2. f1 ⋓ f2 ≘
   elim (IH … Hf) -f /3 width=3 by fcla_push, ex2_intro/
 | #f #n #_ #IH #f1 #f2 #H
   elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
-  elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, le_S_S, le_S, ex2_intro/
+  elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, nle_succ_bi, nle_succ_dx, ex2_intro/
 ]
 qed-.