Few theorems added.`

[helm.git] / matita / library / nat / le_arith.ma

diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma
index a76183063b1e6d211d5c03a75cd1845c844c73aa..ae386d313882f2b37903ae28c60c77dfa9fda072 100644 (file)
--- a/matita/library/nat/le_arith.ma
+++ b/matita/library/nat/le_arith.ma
@@ -51,6 +51,11 @@ intros.change with (O+m \le n+m).
 apply le_plus_l.apply le_O_n.
 qed.
 
+theorem le_plus_n_r :\forall n,m:nat. m \le m + n.
+intros.rewrite > sym_plus.
+apply le_plus_n.
+qed.
+
 theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n.
 intros.rewrite > H.
 rewrite < sym_plus.