update in ground

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

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 2f0f4b658a7251e0f5b69ea023505dfdbb647b6e..75ff371fb108a84e9847927ca670fd2af4c822f5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -50,7 +50,7 @@ lemma niter_plus (A) (f) (n1) (n2):
 /3 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/
 qed.
 
-(* Advanved constructions (semigroup properties) ****************************)
+(* Advanced constructions (semigroup properties) ****************************)
 
 (*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
@@ -65,7 +65,7 @@ qed.
 (*** commutative_plus *)
 lemma nplus_comm: commutative … nplus.
 #m @(nat_ind_succ … m) -m //
-qed-. (**) (* gets in the way with auto *)
+qed-. (* * gets in the way with auto *)
 
 (*** associative_plus *)
 lemma nplus_assoc: associative … nplus.