contribs: some improvements

[helm.git] / helm / software / matita / contribs / RELATIONAL / NPlus / inv.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
index c8450346ec1565231d13080aba8c172c51a18f57..68043c84a6ab65e66512910dcf46f5a0b356eab5 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NPlus/inv.ma
@@ -125,3 +125,10 @@ theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
    subst
  ]; auto new timeout=30.
 qed.
+
+theorem nplus_gen_succ_2_3: \forall p,q,r.
+                            (p + (succ q) == (succ r)) \to p + q == r.
+ intros. 
+ lapply linear nplus_gen_succ_2 to H. decompose. subst.
+ destruct H1. clear H1. subst. auto.
+qed.