-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.apply le_O_n.
simplify. apply le_n.assumption.assumption.
qed.
*)
theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
n \lt p \to \not divides p n!.
simplify. apply le_n.assumption.assumption.
qed.
*)
theorem prime_to_not_divides_fact: \forall p:nat. prime p \to \forall n:nat.
n \lt p \to \not divides p n!.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (j-i).
-apply divides_to_le.simplify.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
+apply (le_to_not_lt p (j-i)).
+apply divides_to_le.unfold lt.
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
-apply trans_lt ? (S O).simplify.apply le_n.assumption.
-apply le_to_not_lt p (i-j).
-apply divides_to_le.simplify.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
+apply (le_to_not_lt p (i-j)).
+apply divides_to_le.unfold lt.
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply divides_times_to_divides.assumption.
rewrite > distr_times_minus.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
apply H4.
qed.
theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
congruent (exp a (pred p)) (S O) p.
intros.
apply H4.
qed.
theorem congruent_exp_pred_SO: \forall p,a:nat. prime p \to \lnot divides p a \to
congruent (exp a (pred p)) (S O) p.
intros.
-apply transitive_congruent p ?
-(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O)).
-apply congruent_pi (\lambda m. a*m).
+apply (transitive_congruent p ?
+(pi (pred (pred p)) (\lambda m. a*m \mod p) (S O))).
+apply (congruent_pi (\lambda m. a*m)).
rewrite > Hcut3.apply congruent_n_n.
rewrite < eq_map_iter_i_pi.
rewrite < eq_map_iter_i_pi.
rewrite > Hcut3.apply congruent_n_n.
rewrite < eq_map_iter_i_pi.
rewrite < eq_map_iter_i_pi.
rewrite > Hcut3.rewrite < times_n_O.
apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
apply le_S_S_to_le.assumption.
assumption.
rewrite > Hcut3.rewrite < times_n_O.
apply mod_O_n.apply sym_eq.apply le_n_O_to_eq.
apply le_S_S_to_le.assumption.
assumption.