apply le_S_S_to_le.
change with ((S i) \mod (S n) < S n).
apply lt_mod_m_m.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
unfold injn.intros.
apply inj_S.
rewrite < (lt_to_eq_mod i (S n)).
(* i < n, j< n *)
rewrite < mod_S.
rewrite < mod_S.
-apply H2.simplify.apply le_S_S.apply le_O_n.
+apply H2.unfold lt.apply le_S_S.apply le_O_n.
rewrite > lt_to_eq_mod.
-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.
rewrite > lt_to_eq_mod.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
(* i < n, j=n *)
unfold S_mod in H2.
simplify.
rewrite < (mod_n_n (S n)).
rewrite < H4 in \vdash (? ? ? (? %?)).
rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
rewrite > lt_to_eq_mod.
-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.
(* i = n, j < n *)
elim Hcut1.
apply False_ind.
rewrite < (mod_n_n (S n)).
rewrite < H3 in \vdash (? ? (? %?) ?).
rewrite < mod_S.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
rewrite > lt_to_eq_mod.
-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.
(* i = n, j= n*)
rewrite > H3.
rewrite > H4.
reflexivity.
apply le_to_or_lt_eq.assumption.
apply le_to_or_lt_eq.assumption.
-simplify.apply le_S_S.assumption.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
+unfold lt.apply le_S_S.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!.
-intros 3.elim n.simplify.intros.
+intros 3.elim n.unfold Not.intros.
apply (lt_to_not_le (S O) p).
unfold prime in H.elim H.
-assumption.apply divides_to_le.simplify.apply le_n.
+assumption.apply divides_to_le.unfold lt.apply le_n.
assumption.
change with (divides p ((S n1)*n1!) \to False).
intro.
cut (divides p (S n1) \lor divides p n1!).
elim Hcut.apply (lt_to_not_le (S n1) p).
assumption.
-apply divides_to_le.simplify.apply le_S_S.apply le_O_n.
+apply divides_to_le.unfold lt.apply le_S_S.apply le_O_n.
assumption.apply H1.
-apply (trans_lt ? (S n1)).simplify. apply le_n.
+apply (trans_lt ? (S n1)).unfold lt. apply le_n.
assumption.assumption.
apply divides_times_to_divides.
assumption.assumption.
apply (trans_le ? p).
change with (mod (a*i) p < p).
apply lt_mod_m_m.
-simplify in H.elim H.
-simplify.apply (trans_le ? (S (S O))).
+unfold prime in H.elim H.
+unfold lt.apply (trans_le ? (S (S O))).
apply le_n_Sn.assumption.
rewrite < S_pred.apply le_n.
unfold prime in H.
elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
unfold injn.intros.
apply (nat_compare_elim i j).
(* i < j *)
intro.
absurd (j-i \lt p).
-simplify.
+unfold lt.
rewrite > (S_pred p).
apply le_S_S.
apply le_plus_to_minus.
apply le_plus_n.
unfold prime in H.
elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
apply (le_to_not_lt p (j-i)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
apply le_SO_minus.assumption.
cut (divides p a \lor divides p (j-i)).
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
apply sym_eq.
apply H4.
(* i = j *)
(* j < i *)
intro.
absurd (i-j \lt p).
-simplify.
+unfold lt.
rewrite > (S_pred p).
apply le_S_S.
apply le_plus_to_minus.
apply le_plus_n.
unfold prime in H.
elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
apply (le_to_not_lt p (i-j)).
-apply divides_to_le.simplify.
+apply divides_to_le.unfold lt.
apply le_SO_minus.assumption.
cut (divides p a \lor divides p (i-j)).
elim Hcut.apply False_ind.apply H1.assumption.assumption.
apply eq_mod_to_divides.
unfold prime in H.
elim H.
-apply (trans_lt ? (S O)).simplify.apply le_n.assumption.
+apply (trans_lt ? (S O)).unfold lt.apply le_n.assumption.
apply H4.
qed.
apply le_S_S_to_le.rewrite < S_pred.
unfold prime in H.elim H.assumption.assumption.
unfold prime in H.elim H.apply (trans_lt ? (S O)).
-simplify.apply le_n.assumption.
+unfold lt.apply le_n.assumption.
cut (O < a \lor O = a).
elim Hcut.assumption.
apply False_ind.apply H1.