(* boolean divides *)
definition divides_b : nat \to nat \to bool \def
\lambda n,m :nat. (eqb (m \mod n) O).
-
+
theorem divides_b_to_Prop :
\forall n,m:nat. O < n \to
match divides_b n m with
intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
qed.
-theorem divides_b_true_to_divides :
+theorem divides_b_true_to_divides1:
\forall n,m:nat. O < n \to
(divides_b n m = true ) \to n \divides m.
intros.
assumption.
qed.
-theorem divides_b_false_to_not_divides :
+theorem divides_b_true_to_divides:
+\forall n,m:nat. divides_b n m = true \to n \divides m.
+intros 2.apply (nat_case n)
+ [apply (nat_case m)
+ [intro.apply divides_n_n
+ |simplify.intros.apply False_ind.
+ apply not_eq_true_false.apply sym_eq.assumption
+ ]
+ |intros.
+ apply divides_b_true_to_divides1
+ [apply lt_O_S|assumption]
+ ]
+qed.
+
+theorem divides_b_false_to_not_divides1:
\forall n,m:nat. O < n \to
(divides_b n m = false ) \to n \ndivides m.
intros.
assumption.
qed.
+theorem divides_b_false_to_not_divides:
+\forall n,m:nat. divides_b n m = false \to n \ndivides m.
+intros 2.apply (nat_case n)
+ [apply (nat_case m)
+ [simplify.unfold Not.intros.
+ apply not_eq_true_false.assumption
+ |unfold Not.intros.elim H1.
+ apply (not_eq_O_S m1).apply sym_eq.
+ assumption
+ ]
+ |intros.
+ apply divides_b_false_to_not_divides1
+ [apply lt_O_S|assumption]
+ ]
+qed.
+
theorem decidable_divides: \forall n,m:nat.O < n \to
decidable (n \divides m).
intros.unfold decidable.
reflexivity.
qed.
+theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n m))
+ [assumption
+ |apply False_ind.
+ elim H1.
+ rewrite < H2 in H1.
+ simplify in H1.
+ apply (lt_to_not_eq O n H).
+ apply sym_eq.
+ apply eqb_true_to_eq.
+ assumption
+ ]
+qed.
+
(* divides and pi *)
theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat.
m \le i \to i \le n+m \to f i \divides pi n f m.
(S O) < i \to i \le n \to i \ndivides S n!.
intros.
apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
unfold divides_b.
-rewrite > mod_S_fact.simplify.reflexivity.
-assumption.assumption.
+rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption].
qed.
(* prime *)
unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
qed.
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
(* smallest factor *)
definition smallest_factor : nat \to nat \def
\lambda n:nat.
apply (witness ? ? (S O)). simplify.reflexivity.
intros.
apply divides_b_true_to_divides.
-apply (lt_O_smallest_factor ? H).
change with
(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1))
(\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
theorem le_smallest_factor_n :
\forall n:nat. smallest_factor n \le n.
-intro.apply (nat_case n).simplify.reflexivity.
-intro.apply (nat_case m).simplify.reflexivity.
+intro.apply (nat_case n).simplify.apply le_n.
+intro.apply (nat_case m).simplify.apply le_n.
intro.apply divides_to_le.
unfold lt.apply le_S_S.apply le_O_n.
apply divides_smallest_factor_n.
intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
intros.
apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b.
apply (lt_min_aux_to_false
(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
cut ((S(S O)) = (S(S m1)-m1)).