From 472cb969d9a01a6d24eabc39ba20d1dc6adf1b04 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 3 Sep 2014 14:59:43 +0000
Subject: [PATCH] - the PARTIAL COMMIT continues, we issue the "reduction"
 component

---
 .../basic_2/etc/sta/{da_aaa.ma => da_aaa.etc} |  0
 .../basic_2/etc/sta/{da_sta.ma => da_sta.etc} |  0
 .../basic_2/etc/sta/{lstas.ma => lstas.etc}   |  0
 .../etc/sta/{lstas_aaa.ma => lstas_aaa.etc}   |  0
 .../etc/sta/{lstas_alt.ma => lstas_alt.etc}   |  0
 .../etc/sta/{lstas_da.ma => lstas_da.etc}     |  0
 .../etc/sta/{lstas_lift.ma => lstas_lift.etc} |  0
 .../sta/{lstas_lstas.ma => lstas_lstas.etc}   |  0
 .../basic_2/etc/sta/{sta.ma => sta.etc}       |  0
 .../etc/sta/{sta_aaa.ma => sta_aaa.etc}       |  0
 .../etc/sta/{sta_lift.ma => sta_lift.etc}     |  0
 .../sta/{sta_llpx_sn.ma => sta_llpx_sn.etc}   |  0
 .../etc/sta/{sta_sta.ma => sta_sta.etc}       |  0
 .../sta/{statictype_5.ma => statictype_5.etc} |  0
 ...pestaralt_6.ma => statictypestaralt_6.etc} |  0
 .../lambdadelta/basic_2/reduction/cpr.ma      | 15 +++++++
 .../lambdadelta/basic_2/reduction/cpx_lift.ma | 31 ++++++++-----
 .../lambdadelta/basic_2/reduction/fpb_lift.ma |  2 +-
 .../lambdadelta/basic_2/unfold/lstas_lift.ma  |  4 --
 .../basic_2/unfold/lstas_llpx_sn.ma           | 44 +++++++++++++++++++
 .../lambdadelta/ground_2/lib/arith.ma         |  7 +++
 21 files changed, 86 insertions(+), 17 deletions(-)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{da_aaa.ma => da_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{da_sta.ma => da_sta.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas.ma => lstas.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas_aaa.ma => lstas_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas_alt.ma => lstas_alt.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas_da.ma => lstas_da.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas_lift.ma => lstas_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{lstas_lstas.ma => lstas_lstas.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{sta.ma => sta.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{sta_aaa.ma => sta_aaa.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{sta_lift.ma => sta_lift.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{sta_llpx_sn.ma => sta_llpx_sn.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{sta_sta.ma => sta_sta.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{statictype_5.ma => statictype_5.etc} (100%)
 rename matita/matita/contribs/lambdadelta/basic_2/etc/sta/{statictypestaralt_6.ma => statictypestaralt_6.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_sta.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_sta.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_sta.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/da_sta.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_alt.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_alt.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_alt.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_da.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_da.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_da.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_da.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lstas.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lstas.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/lstas_lstas.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_llpx_sn.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_llpx_sn.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_llpx_sn.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictype_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictype_5.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictype_5.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictype_5.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictypestaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictypestaralt_6.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictypestaralt_6.ma
rename to matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictypestaralt_6.etc
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
index 6db05fe53..d2034f9d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
@@ -15,6 +15,7 @@
 include "basic_2/notation/relations/pred_4.ma".
 include "basic_2/grammar/genv.ma".
 include "basic_2/static/lsubr.ma".
+include "basic_2/unfold/lstas.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
 
@@ -93,6 +94,20 @@ lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓓV) →
 ]
 qed-.
 
+fact lstas_cpr_aux: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l] T2 →
+                    l = 0 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+#h #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2 -l
+/3 width=1 by cpr_eps, cpr_flat, cpr_bind/
+[ #G #L #l #k #H0 destruct normalize //
+| #G #L #K #V1 #V2 #W2 #i #l #HLK #_ #HVW2 #IHV12 #H destruct
+  /3 width=6 by cpr_delta/
+| #G #L #K #V1 #V2 #W2 #i #l #_ #_ #_ #_ <plus_n_Sm #H destruct
+]
+qed-.
+
+lemma lstas_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*[h, 0] T2 → ⦃G, L⦄ ⊢ T1 ➡ T2.
+/2 width=4 by lstas_cpr_aux/ qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 fact cpr_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index e3ac0af19..f0337ff95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -14,7 +14,6 @@
 
 include "basic_2/substitution/drop_drop.ma".
 include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/static/sta.ma".
 include "basic_2/static/da.ma".
 include "basic_2/reduction/cpx.ma".
 
@@ -22,21 +21,29 @@ include "basic_2/reduction/cpx.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma sta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h] T2 →
-               ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2
-[ /3 width=4 by cpx_st, da_inv_sort/
-| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
+fact sta_cpx_aux: ∀h,g,G,L,T1,T2,l2,l1. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → l2 = 1 →
+                  ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #l2 #l1 #H elim H -G -L -T1 -T2 -l2
+[ #G #L #l2 #k #H0 destruct normalize
+  /3 width=4 by cpx_st, da_inv_sort/
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #_ #HVW2 #IHV12 #H0 #H destruct
   elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
-| #G #L #K #W1 #W2 #V1 #i #HLK #_ #HWV1 #IHW12 #H
-  elim (da_inv_lref … H) -H * #K0 #W0 [| #l1 ] #HLK0
-  lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
+| #G #L #K #V1 #V2 #i #_ #_ #_ #H destruct
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #HV12 #HVW2 #_ #H0 #H
+  lapply (discr_plus_xy_y … H0) -H0 #H0 destruct
+  elim (da_inv_lref … H) -H * #K0 #V0 [| #l1 ] #HLK0
+  lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
+  /4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/
 | /4 width=2 by cpx_bind, da_inv_bind/
 | /4 width=3 by cpx_flat, da_inv_flat/
 | /4 width=3 by cpx_eps, da_inv_flat/
 ]
-qed.
+qed-.
+
+lemma sta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
+               ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/2 width=3 by sta_cpx_aux/ qed.
 
 (* Relocation properties ****************************************************)
 
@@ -155,7 +162,7 @@ lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T
 qed-.
 
 lemma fqu_sta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                     ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h] U2 →
+                     ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
                      ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
 /3 width=5 by fqu_cpx_trans, sta_cpx/ qed-.
@@ -170,7 +177,7 @@ lemma fquq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L
 qed-.
 
 lemma fquq_sta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h] U2 →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
                       ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
 /3 width=5 by fquq_cpx_trans, sta_cpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma
index 86a0ad79e..777a944fb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_lift.ma
@@ -20,6 +20,6 @@ include "basic_2/reduction/fpb.ma".
 (* Advanced properties ******************************************************)
 
 lemma sta_fpb: ∀h,g,G,L,T1,T2,l.
-                ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T2 →
+                ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
                 ⦃G, L, T1⦄ ≽[h, g] ⦃G, L, T2⦄.
 /3 width=4 by fpb_cpx, sta_cpx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma
index 9239d34df..aea1d9f85 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_lift.ma
@@ -115,10 +115,6 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
-* /2 width=1 by conj/ #x #y normalize #H destruct
-qed-.
-
 lemma lstas_split_aux: ∀h,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ∀l1,l2. l = l1 + l2 →
                        ∃∃T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T & ⦃G, L⦄ ⊢ T •*[h, l2] T2.
 #h #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2 -l
diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma
new file mode 100644
index 000000000..afa9d46d3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_llpx_sn.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/multiple/llpx_sn_drop.ma".
+include "basic_2/unfold/lstas.ma".
+
+(* NAT-ITERATED STATIC TYPE ASSIGNMENT FOR TERMS ****************************)
+
+(* Properties on lazy sn pointwise extensions *******************************)
+
+lemma lstas_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R →
+                          ∀h,G,l. s_r_confluent1 … (lstas h l G) (llpx_sn R 0).
+#R #H1R #H2R #h #G #l #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 -l
+[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/
+| #G #Ls #Ks #V1s #V2s #W2s #i #l #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+  #Kd #V1d #HLKd #HV1s #HV1sd
+  lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs
+  lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd
+  @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| //
+| #G #Ls #Ks #V1s #V2s #W2s #i #l #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H
+  #Kd #V1d #HLKd #HV1s #HV1sd
+  lapply (drop_fwd_drop2 … HLKs) -HLKs #HLKs
+  lapply (drop_fwd_drop2 … HLKd) -HLKd #HLKd
+  @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *)
+| #a #I #G #Ls #V #T1 #T2 #l #_ #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H
+  /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/
+| #G #Ls #V #T1 #T2 #l #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+  /3 width=1 by llpx_sn_flat/
+| #G #Ls #V #T1 #T2 #l #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H
+  /3 width=1 by llpx_sn_flat/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 203727730..93fb86d42 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -111,6 +111,9 @@ qed.
 
 (* Inversion & forward lemmas ***********************************************)
 
+lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
+// qed-.
+
 lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
 /2 width=1 by monotonic_pred/ qed-.
 
@@ -150,6 +153,10 @@ lemma discr_x_minus_xy: ∀x,y. x = x - y → x = 0 ∨ y = 0.
 #H destruct
 qed-.
 
+lemma zero_eq_plus: ∀x,y. 0 = x + y → 0 = x ∧ 0 = y.
+* /2 width=1 by conj/ #x #y normalize #H destruct
+qed-.
+
 (* Iterators ****************************************************************)
 
 (* Note: see also: lib/arithemetics/bigops.ma *)
-- 
2.39.2