arithmetics for λδ

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_succ_tri.ma

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 e3be44c68b72dd78038815005220a494332e43e1..b8c1191b91c20c2d9ce097dc4d4a21a495a2a95d 100644 (file)
--- 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.