X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=44c3119fae1fad9be401452f9c4a667eb813a050;hb=ef3bdc4be26f6518a82a79c64e986253f7aeaa3c;hp=8f7acf2b20003066f80d67cf94af158d20d20ab2;hpb=35653f628dc3a3e665fee01acc19c660c9d555e3;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 8f7acf2b2..44c3119fa 100644
--- 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.