set "baseuri" "cic:/matita/nat/log".
include "datatypes/constructors.ma".
-include "nat/primes.ma".
include "nat/exp.ma".
+include "nat/lt_arith.ma".
+include "nat/primes.ma".
(* this definition of log is based on pairs, with a remainder *)
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 ?.
+apply not_eq_O_S m1.
rewrite > H5.reflexivity.
qed.