lambda_delta: global environments handling: redefined and first results

[helm.git] / matita / matita / lib / arithmetics / nat.ma

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 8f7acf2b20003066f80d67cf94af158d20d20ab2..44c3119fae1fad9be401452f9c4a667eb813a050 100644 (file)
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -132,6 +132,9 @@ theorem assoc_plus1: ∀a,b,c. c + (b + a) = b + c + a.
 theorem injective_plus_r: ∀n:nat.injective nat nat (λm.n+m).
 #n (elim n) normalize /3/ qed.
 
+theorem injective_plus_l: ∀n:nat.injective nat nat (λm.m+n). 
+/2/ qed.
+
 theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
 /2/ qed.