update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
index 5e131af37b8f211f269a83f77eca4e5f1ebb3fd9..d54738f250b4100fea5bbdde0c20518572aad361 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le_plus.ma
@@ -15,9 +15,9 @@
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_le.ma".
 
-(* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
+(* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
 
-(* Constructions with nplus ***********************************************************)
+(* Constructions with nplus *************************************************)
 
 (*** monotonic_le_plus_l *)
 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.