]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/library/nat/log.ma
* Obsolete debugging comments removed
[helm.git] / helm / matita / library / nat / log.ma
index 3babb5c75151fe36f0cf098e055d39294164eb22..51d0108d97d89d937a488c68d6fbb7bc1e0a5323 100644 (file)
@@ -175,7 +175,7 @@ apply lt_div_n_m_n.assumption.assumption.assumption.
 intros.
 change with (\lnot (mod n1 m = O)).
 rewrite > H4.
-(* META NOT FOUND !!!  
+(* Andrea: META NOT FOUND !!!  
 rewrite > sym_eq. *)
 simplify.intro.
 apply not_eq_O_S m1.