rewrite > H1.
change with (divides_b (smallest_factor n) n = true).
apply divides_to_divides_b_true.
-apply (trans_lt ? (S O)).simplify. apply le_n.
+apply (trans_lt ? (S O)).unfold lt. apply le_n.
apply lt_SO_smallest_factor.assumption.
apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). simplify. apply le_n. assumption.
+apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
apply prime_to_nth_prime.
apply prime_smallest_factor_n.assumption.
qed.
theorem lt_O_defactorize_aux: \forall f:nat_fact.\forall i:nat.
O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt.
rewrite > times_n_SO.
apply le_times.
change with (O < nth_prime i).
change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
-simplify.
+simplify.unfold lt.
rewrite > times_n_SO.
apply le_times.
change with (O < exp (nth_prime i) n).
theorem lt_SO_defactorize_aux: \forall f:nat_fact.\forall i:nat.
S O < defactorize_aux f i.
-intro.elim f.simplify.
+intro.elim f.simplify.unfold lt.
rewrite > times_n_SO.
apply le_times.
change with (S O < nth_prime i).
change with (O < exp (nth_prime i) n).
apply lt_O_exp.
apply lt_O_nth_prime_n.
-simplify.
+simplify.unfold lt.
rewrite > times_n_SO.
rewrite > sym_times.
apply le_times.
cut (O < r \lor O = r).
elim Hcut1.assumption.absurd (n1 = O).
rewrite > Hcut.rewrite < H4.reflexivity.
-simplify. intro.apply (not_le_Sn_O O).
+unfold Not. intro.apply (not_le_Sn_O O).
rewrite < H5 in \vdash (? ? %).assumption.
apply le_to_or_lt_eq.apply le_O_n.
cut ((S O) < r \lor (S O) \nlt r).
apply (nat_case n).
left.split.assumption.reflexivity.
intro.right.rewrite > Hcut2.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
cut (r \lt (S O) \or r=(S O)).
elim Hcut2.absurd (O=r).
apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
-simplify.intro.
+unfold Not.intro.
cut (O=n1).
apply (not_le_Sn_O O).
rewrite > Hcut3 in \vdash (? ? %).
elim Hcut2.assumption.
absurd (nth_prime p \divides S (S m1)).
apply (divides_max_prime_factor_n (S (S m1))).
-simplify.apply le_S_S.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
cut ((S(S m1)) = r).
rewrite > Hcut3 in \vdash (? (? ? %)).
change with (nth_prime p \divides r \to False).
intro.
apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
apply lt_SO_nth_prime_n.
-simplify.apply le_S_S.apply le_O_n.apply le_n.
+unfold lt.apply le_S_S.apply le_O_n.apply le_n.
assumption.
apply divides_to_mod_O.apply lt_O_nth_prime_n.assumption.
rewrite > times_n_SO in \vdash (? ? ? %).
elim Hcut2.
right.
apply (p_ord_to_lt_max_prime_factor1 (S(S m1)) ? q r).
-simplify.apply le_S_S. apply le_O_n.
+unfold lt.apply le_S_S. apply le_O_n.
apply le_n.
assumption.assumption.
cut (r=(S O)).
apply (nat_case p).
left.split.assumption.reflexivity.
intro.right.rewrite > Hcut3.
-simplify.apply le_S_S.apply le_O_n.
+simplify.unfold lt.apply le_S_S.apply le_O_n.
cut (r \lt (S O) \or r=(S O)).
elim Hcut3.absurd (O=r).
apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
-simplify.intro.
+unfold Not.intro.
apply (not_le_Sn_O O).
rewrite > H3 in \vdash (? ? %).assumption.assumption.
apply (le_to_or_lt_eq r (S O)).
\forall p,q,m:nat. prime p \to prime q \to
p \divides q \sup m \to p = q.
intros.
-simplify in H1.
+unfold prime in H1.
elim H1.apply H4.
apply (divides_exp_to_divides p q m).
assumption.assumption.
-simplify in H.elim H.assumption.
+unfold prime in H.elim H.assumption.
qed.
theorem not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
apply (not_le_Sn_n i).rewrite > Hcut1 in \vdash (? ? %).assumption.
apply (injective_nth_prime ? ? H4).
apply (H i (S j)).
-apply (trans_lt ? j).assumption.simplify.apply le_n.
+apply (trans_lt ? j).assumption.unfold lt.apply le_n.
assumption.
apply divides_times_to_divides.
apply prime_nth_prime.assumption.
lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
\lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
intros.
-simplify.rewrite < plus_n_O.
+simplify.unfold Not.rewrite < plus_n_O.
intro.
apply (not_divides_defactorize_aux f i (S i) ?).
-simplify.apply le_n.
+unfold lt.apply le_n.
rewrite > H.
rewrite > assoc_times.
apply (witness ? ? ((exp (nth_prime i) n)*(defactorize_aux g (S i)))).