X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fnat.ma;h=56935028f65015812b79fdc15fb8762b012d14cf;hb=9def1b8a298aac85a7abdc75c4a33657fe7e6df7;hp=edb99b8c0c9dac85517e253e9282d7f34597bd89;hpb=c16905138e385d30856d587f07c396a3cab301ed;p=helm.git

diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index edb99b8c0..56935028f 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -305,6 +305,10 @@ lemma lt_to_le: ∀x,y. x < y → x ≤ y.
 lemma inv_eq_minus_O: ∀x,y. x - y = 0 → x ≤ y.
 // qed-.
 
+lemma le_x_times_x: ∀x. x ≤ x * x.
+#x elim x -x //
+qed.
+
 (* lt *)
 
 theorem transitive_lt: transitive nat lt.