X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_succ_tri.ma;h=b8c1191b91c20c2d9ce097dc4d4a21a495a2a95d;hp=e3be44c68b72dd78038815005220a494332e43e1;hb=21de0d35017656c5a55528390b54b0b2ae395b44;hpb=68e028d053806177e218ee1a5f8778d3011bef83

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
index e3be44c68..b8c1191b9 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
@@ -17,7 +17,17 @@ include "ground/arith/nat_succ.ma".
 
 (* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
 
-(* Rewrites with ntri *******************************************************)
+(* Constructions with ntri **************************************************)
+
+lemma ntri_zero_succ (A) (a1) (a2) (a3) (n):
+      a1 = ntri A (𝟎) (↑n) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
+
+lemma ntri_succ_zero (A) (a1) (a2) (a3) (n):
+      a3 = ntri A (↑n) (𝟎) a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
 
 lemma ntri_succ_bi (A) (a1) (a2) (a3) (n1) (n2):
       ntri A (n1) (n2) a1 a2 a3 = ntri A (↑n1) (↑n2) a1 a2 a3.