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 *)
rewrite < H2.
rewrite > sym_times.
rewrite < div_mod.reflexivity.
-intros.simplify.apply plus_n_O.
assumption.assumption.
+intros.simplify.apply plus_n_O.
qed.
theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
cut div ((exp m (S n1))*n) m = (exp m n1)*n.
rewrite > Hcut1.
rewrite > H2 m1. simplify.reflexivity.
+apply le_S_S_to_le.assumption.
(* div_exp *)
change with div (m*(exp m n1)*n) m = (exp m n1)*n.
rewrite > assoc_times.
assumption.
simplify.rewrite > assoc_times.
apply witness ? ? ((exp m n1)*n).reflexivity.
-apply le_S_S_to_le.assumption.
qed.
theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
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.