definition distributive2: \forall A,B:Type.\forall f:A \to B \to B.
\forall g: B\to B\to B. Prop
\def \lambda A,B.\lambda f,g.\forall x:A.\forall y,z:B. f x (g y z) = g (f x y) (f x z).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/chinese_reminder".
+
+include "nat/exp.ma".
+include "nat/gcd.ma".
+include "nat/permutation.ma".
+include "nat/congruence.ma".
+
+theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to
+gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
+intros.
+cut \exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O).
+elim Hcut.elim H3.elim H4.
+apply ex_intro nat ? ((a+b*m)*a1*n-b*a2*m).
+split.
+(* congruent to a *)
+cut a1*n = a2*m + (S O).
+rewrite > assoc_times.
+rewrite > Hcut1.
+rewrite < sym_plus ? (a2*m).
+rewrite > distr_times_plus.
+rewrite < times_n_SO.
+rewrite > assoc_plus.
+rewrite < assoc_times.
+rewrite < times_plus_l.
+rewrite > eq_minus_plus_plus_minus.
+rewrite < times_minus_l.
+rewrite > sym_plus.
+apply eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2).
+assumption.reflexivity.
+apply le_times_l.
+apply trans_le ? ((a+b*m)*a2).
+apply le_times_l.
+apply trans_le ? (b*m).
+rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.assumption.
+apply le_plus_n.
+apply le_plus_n.
+apply minus_to_plus.
+apply lt_to_le.
+change with (O + a2*m < a1*n).
+apply lt_minus_to_plus.
+rewrite > H5.simplify.apply le_n.
+assumption.
+(* congruent to b *)
+cut a2*m = a1*n - (S O).
+rewrite > assoc_times b a2.
+rewrite > Hcut1.
+rewrite > distr_times_minus.
+rewrite < assoc_times.
+rewrite < eq_plus_minus_minus_minus.
+rewrite < times_n_SO.
+rewrite < times_minus_l.
+rewrite < sym_plus.
+apply eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1).
+assumption.reflexivity.
+rewrite > assoc_times.
+apply le_times_r.
+apply trans_le ? (a1*n - a2*m).
+rewrite > H5.apply le_n.
+apply le_minus_m ? (a2*m).
+apply le_times_l.
+apply le_times_l.
+apply trans_le ? (b*m).
+rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.assumption.
+apply le_plus_n.
+apply sym_eq. apply plus_to_minus.
+rewrite > sym_plus.
+apply minus_to_plus.
+apply lt_to_le.
+change with (O + a2*m < a1*n).
+apply lt_minus_to_plus.
+rewrite > H5.simplify.apply le_n.
+assumption.
+(* and now the symmetric case; the price to pay for working
+ in nat instead than Z *)
+apply ex_intro nat ? ((b+a*n)*a2*m-a*a1*n).
+split.
+(* congruent to a *)
+cut a1*n = a2*m - (S O).
+rewrite > assoc_times a a1.
+rewrite > Hcut1.
+rewrite > distr_times_minus.
+rewrite < assoc_times.
+rewrite < eq_plus_minus_minus_minus.
+rewrite < times_n_SO.
+rewrite < times_minus_l.
+rewrite < sym_plus.
+apply eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2).
+assumption.reflexivity.
+rewrite > assoc_times.
+apply le_times_r.
+apply trans_le ? (a2*m - a1*n).
+rewrite > H5.apply le_n.
+apply le_minus_m ? (a1*n).
+rewrite > assoc_times.rewrite > assoc_times.
+apply le_times_l.
+apply trans_le ? (a*n).
+rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.assumption.
+apply le_plus_n.
+apply sym_eq.apply plus_to_minus.
+rewrite > sym_plus.
+apply minus_to_plus.
+apply lt_to_le.
+change with (O + a1*n < a2*m).
+apply lt_minus_to_plus.
+rewrite > H5.simplify.apply le_n.
+assumption.
+(* congruent to a *)
+cut a2*m = a1*n + (S O).
+rewrite > assoc_times.
+rewrite > Hcut1.
+rewrite > sym_plus (a1*n).
+rewrite > distr_times_plus.
+rewrite < times_n_SO.
+rewrite < assoc_times.
+rewrite > assoc_plus.
+rewrite < times_plus_l.
+rewrite > eq_minus_plus_plus_minus.
+rewrite < times_minus_l.
+rewrite > sym_plus.
+apply eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1).
+assumption.reflexivity.
+apply le_times_l.
+apply trans_le ? ((b+a*n)*a1).
+apply le_times_l.
+apply trans_le ? (a*n).
+rewrite > times_n_SO in \vdash (? % ?).
+apply le_times_r.
+assumption.
+apply le_plus_n.
+apply le_plus_n.
+apply minus_to_plus.
+apply lt_to_le.
+change with (O + a1*n < a2*m).
+apply lt_minus_to_plus.
+rewrite > H5.simplify.apply le_n.
+assumption.
+(* proof of the cut *)
+rewrite < H2.
+apply eq_minus_gcd.
+qed.
+
+theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to
+gcd n m = (S O) \to
+ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
+ (x < m*n)).
+intros.elim and_congruent_congruent m n a b.
+elim H3.
+apply ex_intro ? ? (a1 \mod (m*n)).
+split.split.
+apply transitive_congruent m ? a1.
+unfold congruent.
+apply sym_eq.
+change with congruent a1 (a1 \mod (m*n)) m.
+rewrite < sym_times.
+apply congruent_n_mod_times.
+assumption.assumption.assumption.
+apply transitive_congruent n ? a1.
+unfold congruent.
+apply sym_eq.
+change with congruent a1 (a1 \mod (m*n)) n.
+apply congruent_n_mod_times.
+assumption.assumption.assumption.
+apply lt_mod_m_m.
+rewrite > times_n_O O.
+apply lt_times.assumption.assumption.
+assumption.assumption.assumption.
+qed.
+
+definition cr_pair : nat \to nat \to nat \to nat \to nat \def
+\lambda n,m,a,b.
+min (pred (n*m)) (\lambda x. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
+
+theorem cr_pair1: cr_pair (S (S O)) (S (S (S O))) O O = O.
+reflexivity.
+qed.
+
+theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
+simplify.
+reflexivity.
+qed.
+
+theorem cr_pair3: cr_pair (S(S O)) (S(S(S O))) (S O) (S(S O)) = (S(S(S(S(S O))))).
+reflexivity.
+qed.
+
+theorem cr_pair4: cr_pair (S(S(S(S(S O))))) (S(S(S(S(S(S(S O))))))) (S(S(S O))) (S(S O)) =
+(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S O))))))))))))))))))))))).
+reflexivity.
+qed.
+
+theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to
+gcd n m = (S O) \to
+(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
+intros.
+cut andb (eqb ((cr_pair m n a b) \mod m) a)
+ (eqb ((cr_pair m n a b) \mod n) b) = true.
+generalize in match Hcut.
+apply andb_elim.
+apply eqb_elim.intro.
+rewrite > H3.
+change with
+eqb ((cr_pair m n a b) \mod n) b = true
+\to a = a \land (cr_pair m n a b) \mod n = b.
+intro.split.reflexivity.
+apply eqb_true_to_eq.assumption.
+intro.
+change with false = true \to
+(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
+intro.apply False_ind.
+apply not_eq_true_false.apply sym_eq.assumption.
+apply f_min_aux_true
+(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n)).
+elim and_congruent_congruent_lt m n a b.
+apply ex_intro ? ? a1.split.split.
+rewrite < minus_n_n.apply le_O_n.
+elim H3.apply le_S_S_to_le.apply trans_le ? (m*n).
+assumption.apply nat_case (m*n).apply le_O_n.
+intro.
+rewrite < pred_Sn.apply le_n.
+elim H3.elim H4.
+apply andb_elim.
+cut a1 \mod m = a.
+cut a1 \mod n = b.
+rewrite > eq_to_eqb_true ? ? Hcut.
+rewrite > eq_to_eqb_true ? ? Hcut1.
+simplify.reflexivity.
+rewrite < lt_to_eq_mod b n.assumption.
+assumption.
+rewrite < lt_to_eq_mod a m.assumption.
+assumption.
+apply le_to_lt_to_lt ? b.apply le_O_n.assumption.
+apply le_to_lt_to_lt ? a.apply le_O_n.assumption.
+assumption.
+qed.
\ No newline at end of file
simplify.assumption.
qed.
+theorem eqb_true_to_eq: \forall n,m:nat.
+eqb n m = true \to n = m.
+intros.
+change with
+match true with
+[ true \Rightarrow n = m
+| false \Rightarrow n \neq m].
+rewrite < H.
+apply eqb_to_Prop.
+qed.
+
+theorem eqb_false_to_not_eq: \forall n,m:nat.
+eqb n m = false \to n \neq m.
+intros.
+change with
+match false with
+[ true \Rightarrow n = m
+| false \Rightarrow n \neq m].
+rewrite < H.
+apply eqb_to_Prop.
+qed.
+
theorem eq_to_eqb_true: \forall n,m:nat.
n = m \to eqb n m = true.
intros.apply (eqb_elim n m).
assumption.
qed.
+theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
+intros.
+apply div_mod_spec_to_eq2 n p (n/p) (n \mod p)
+(n/(m*p)*m + (n \mod (m*p)/p)).
+apply div_mod_spec_div_mod.assumption.
+constructor 1.
+apply lt_mod_m_m.assumption.
+rewrite > times_plus_l.
+rewrite > assoc_plus.
+rewrite < div_mod.
+rewrite > assoc_times.
+rewrite < div_mod.
+reflexivity.
+rewrite > times_n_O O.
+apply lt_times.
+assumption.assumption.assumption.
+qed.
+
theorem congruent_n_mod_n :
\forall n,p:nat. O < p \to congruent n (n \mod p) p.
intros.unfold congruent.
apply mod_mod.assumption.
qed.
+theorem congruent_n_mod_times :
+\forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
+intros.unfold congruent.
+apply mod_times_mod.assumption.assumption.
+qed.
+
theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to
n = r*p+m \to congruent n m p.
intros.unfold congruent.
--- /dev/null
+(**************************************************************************)
+(* __ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/count".
+
+include "nat/relevant_equations.ma".
+include "nat/sigma_and_pi.ma".
+include "nat/permutation.ma".
+
+theorem sigma_f_g : \forall n,m:nat.\forall f,g:nat \to nat.
+sigma n (\lambda p.f p + g p) m = sigma n f m + sigma n g m.
+intros.elim n.
+simplify.reflexivity.
+simplify.rewrite > H.
+rewrite > assoc_plus.
+rewrite < assoc_plus (g (S (n1+m))).
+rewrite > sym_plus (g (S (n1+m))).
+rewrite > assoc_plus (sigma n1 f m).
+rewrite < assoc_plus.
+reflexivity.
+qed.
+
+theorem sigma_plus: \forall n,p,m:nat.\forall f:nat \to nat.
+sigma (S (p+n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
+intros. elim p.
+simplify.
+rewrite < sym_plus n m.reflexivity.
+simplify.
+rewrite > assoc_plus in \vdash (? ? ? %).
+rewrite < H.
+simplify.
+rewrite < plus_n_Sm.
+rewrite > sym_plus n.
+rewrite > assoc_plus.
+rewrite < sym_plus m.
+rewrite < assoc_plus n1.
+reflexivity.
+qed.
+
+theorem sigma_plus1: \forall n,p,m:nat.\forall f:nat \to nat.
+sigma (p+(S n)) f m = sigma p (\lambda x.(f ((S n) + x))) m + sigma n f m.
+intros. elim p.
+simplify.reflexivity.
+simplify.
+rewrite > assoc_plus in \vdash (? ? ? %).
+rewrite < H.
+rewrite < plus_n_Sm.
+rewrite < plus_n_Sm.simplify.
+rewrite < sym_plus n.
+rewrite > assoc_plus.
+rewrite < sym_plus m.
+rewrite < assoc_plus n.
+reflexivity.
+qed.
+
+theorem eq_sigma_sigma : \forall n,m:nat.\forall f:nat \to nat.
+sigma (pred ((S n)*(S m))) f O =
+sigma m (\lambda a.(sigma n (\lambda b.f (b*(S m) + a)) O)) O.
+intro.elim n.simplify.
+rewrite < plus_n_O.
+apply eq_sigma.intros.reflexivity.
+change with
+sigma (m+(S n1)*(S m)) f O =
+sigma m (\lambda a.(f ((S(n1+O))*(S m)+a)) + (sigma n1 (\lambda b.f (b*(S m)+a)) O)) O.
+rewrite > sigma_f_g.
+rewrite < plus_n_O.
+rewrite < H.
+rewrite > S_pred ((S n1)*(S m)).
+apply sigma_plus1.
+simplify.apply le_S_S.apply le_O_n.
+qed.
+
+theorem eq_sigma_sigma1 : \forall n,m:nat.\forall f:nat \to nat.
+sigma (pred ((S n)*(S m))) f O =
+sigma n (\lambda a.(sigma m (\lambda b.f (b*(S n) + a)) O)) O.
+intros.
+rewrite > sym_times.
+apply eq_sigma_sigma.
+qed.
+
+theorem sigma_times: \forall n,m,p:nat.\forall f:nat \to nat.
+(sigma n f m)*p = sigma n (\lambda i.(f i) * p) m.
+intro. elim n.simplify.reflexivity.
+simplify.rewrite < H.
+apply times_plus_l.
+qed.
+
+definition bool_to_nat: bool \to nat \def
+\lambda b. match b with
+[ true \Rightarrow (S O)
+| false \Rightarrow O ].
+
+theorem bool_to_nat_andb: \forall a,b:bool.
+bool_to_nat (andb a b) = (bool_to_nat a)*(bool_to_nat b).
+intros. elim a.elim b.
+simplify.reflexivity.
+reflexivity.
+reflexivity.
+qed.
+
+definition count : nat \to (nat \to bool) \to nat \def
+\lambda n.\lambda f. sigma (pred n) (\lambda n.(bool_to_nat (f n))) O.
+
+theorem count_times:\forall n,m:nat.
+\forall f,f1,f2:nat \to bool.
+\forall g:nat \to nat \to nat.
+\forall g1,g2: nat \to nat.
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g b a) < (S n)*(S m)) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g1 (g b a)) = a) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to (g2 (g b a)) = b) \to
+(\forall a,b:nat. a < (S n) \to b < (S m) \to f (g b a) = andb (f2 b) (f1 a)) \to
+(count ((S n)*(S m)) f) = (count (S n) f1)*(count (S m) f2).
+intros.unfold count.
+rewrite < eq_map_iter_i_sigma.
+rewrite > permut_to_eq_map_iter_i plus assoc_plus sym_plus ? ? ? (\lambda i.g (div i (S n)) (mod i (S n))).
+rewrite > eq_map_iter_i_sigma.
+rewrite > eq_sigma_sigma1.
+apply trans_eq ? ?
+(sigma n (\lambda a.
+ sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O).
+apply eq_sigma.intros.
+apply eq_sigma.intros.
+rewrite > div_mod_spec_to_eq (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i.
+rewrite > div_mod_spec_to_eq2 (i1*(S n) + i) (S n) ((i1*(S n) + i)/(S n)) ((i1*(S n) + i) \mod (S n)) i1 i.
+rewrite > H3.
+apply bool_to_nat_andb.
+simplify.apply le_S_S.assumption.
+simplify.apply le_S_S.assumption.
+apply div_mod_spec_div_mod.
+simplify.apply le_S_S.apply le_O_n.
+constructor 1.simplify.apply le_S_S.assumption.
+reflexivity.
+apply div_mod_spec_div_mod.
+simplify.apply le_S_S.apply le_O_n.
+constructor 1.simplify.apply le_S_S.assumption.
+reflexivity.
+apply trans_eq ? ?
+(sigma n (\lambda n.((bool_to_nat (f1 n)) *
+(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O).
+apply eq_sigma.
+intros.
+rewrite > sym_times.
+apply trans_eq ? ?
+(sigma m (\lambda n.(bool_to_nat (f2 n))*(bool_to_nat (f1 i))) O).
+reflexivity.
+apply sym_eq. apply sigma_times.
+change in match (pred (S n)) with n.
+change in match (pred (S m)) with m.
+apply sym_eq. apply sigma_times.
+unfold permut.
+split.
+intros.
+rewrite < plus_n_O.
+apply le_S_S_to_le.
+rewrite < S_pred in \vdash (? ? %).
+change with ((g (i/(S n)) (i \mod (S n))) \lt (S n)*(S m)).
+apply H.
+apply lt_mod_m_m.
+simplify. apply le_S_S.apply le_O_n.
+apply lt_times_to_lt_l n.
+apply le_to_lt_to_lt ? i.
+rewrite > div_mod i (S n) in \vdash (? ? %).
+rewrite > sym_plus.
+apply le_plus_n.
+simplify. apply le_S_S.apply le_O_n.
+unfold lt.
+rewrite > S_pred in \vdash (? ? %).
+apply le_S_S.
+rewrite > plus_n_O in \vdash (? ? %).
+rewrite > sym_times. assumption.
+rewrite > times_n_O O.
+apply lt_times.
+simplify. apply le_S_S.apply le_O_n.
+simplify. apply le_S_S.apply le_O_n.
+rewrite > times_n_O O.
+apply lt_times.
+simplify. apply le_S_S.apply le_O_n.
+simplify. apply le_S_S.apply le_O_n.
+rewrite < plus_n_O.
+unfold injn.
+intros.
+cut i < (S n)*(S m).
+cut j < (S n)*(S m).
+cut (i \mod (S n)) < (S n).
+cut (i/(S n)) < (S m).
+cut (j \mod (S n)) < (S n).
+cut (j/(S n)) < (S m).
+rewrite > div_mod i (S n).
+rewrite > div_mod j (S n).
+rewrite < H1 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3.
+rewrite < H2 (i \mod (S n)) (i/(S n)) Hcut2 Hcut3 in \vdash (? ? (? % ?) ?).
+rewrite < H1 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5.
+rewrite < H2 (j \mod (S n)) (j/(S n)) Hcut4 Hcut5 in \vdash (? ? ? (? % ?)).
+rewrite > H6.reflexivity.
+simplify. apply le_S_S.apply le_O_n.
+simplify. apply le_S_S.apply le_O_n.
+apply lt_times_to_lt_l n.
+apply le_to_lt_to_lt ? j.
+rewrite > div_mod j (S n) in \vdash (? ? %).
+rewrite > sym_plus.
+apply le_plus_n.
+simplify. apply le_S_S.apply le_O_n.
+rewrite < sym_times. assumption.
+apply lt_mod_m_m.
+simplify. apply le_S_S.apply le_O_n.
+apply lt_times_to_lt_l n.
+apply le_to_lt_to_lt ? i.
+rewrite > div_mod i (S n) in \vdash (? ? %).
+rewrite > sym_plus.
+apply le_plus_n.
+simplify. apply le_S_S.apply le_O_n.
+rewrite < sym_times. assumption.
+apply lt_mod_m_m.
+simplify. apply le_S_S.apply le_O_n.
+unfold lt.
+rewrite > S_pred in \vdash (? ? %).
+apply le_S_S.assumption.
+rewrite > times_n_O O.
+apply lt_times.
+simplify. apply le_S_S.apply le_O_n.
+simplify. apply le_S_S.apply le_O_n.
+unfold lt.
+rewrite > S_pred in \vdash (? ? %).
+apply le_S_S.assumption.
+rewrite > times_n_O O.
+apply lt_times.
+simplify. apply le_S_S.apply le_O_n.
+simplify. apply le_S_S.apply le_O_n.
+intros.
+apply False_ind.
+apply not_le_Sn_O m1 H4.
+qed.
apply le_to_or_lt_eq.apply le_O_n.
qed.
+theorem divides_gcd_mod: \forall m,n:nat. O < n \to O < m \to
+divides (gcd m n) (gcd n (m \mod n)).
+intros.
+apply divides_d_gcd.
+apply divides_mod.assumption.
+apply divides_gcd_n.
+apply divides_gcd_m.
+apply divides_gcd_m.
+qed.
+
+theorem divides_mod_gcd: \forall m,n:nat. O < n \to O < m \to
+divides (gcd n (m \mod n)) (gcd m n) .
+intros.
+apply divides_d_gcd.
+apply divides_gcd_n.
+apply divides_mod_to_divides ? ? n.
+assumption.
+apply divides_gcd_m.
+apply divides_gcd_n.
+qed.
+
+(* gcd and primes *)
+
theorem prime_to_gcd_SO: \forall n,m:nat. prime n \to n \ndivides m \to
gcd n m = (S O).
intros.simplify in H.change with (gcd n m = (S O)).
assumption.
qed.
+theorem le_min_aux_r : \forall f:nat \to bool.
+\forall n,off:nat. (min_aux off n f) \le n.
+intros.
+elim off.simplify.rewrite < minus_n_O.
+elim (f n).simplify.apply le_n.
+simplify.apply le_n.
+simplify.elim (f (n -(S n1))).
+simplify.apply le_plus_to_minus.
+rewrite < sym_plus.apply le_plus_n.
+simplify.assumption.
+qed.
rewrite > plus_n_Sm.assumption.
qed.
+(* minus and lt - to be completed *)
+theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
+intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
+simplify.intros.apply False_ind.apply not_le_Sn_O n H.
+simplify.intros.
+apply le_S_S.
+rewrite < plus_n_Sm.
+apply H.apply H1.
+qed.
theorem distributive_times_minus: distributive nat times minus.
simplify.
theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
\def distributive_times_minus.
+theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
+intros.
+apply plus_to_minus.
+rewrite > sym_plus in \vdash (? ? ? %).
+rewrite > assoc_plus.
+rewrite < plus_minus_m_m.
+reflexivity.assumption.
+qed.
+
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
cut (m+p \le n \or m+p \nleq n).
--- /dev/null
+(**************************************************************************)
+(* __ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| A.Asperti, C.Sacerdoti Coen, *)
+(* ||A|| E.Tassi, S.Zacchiroli *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU Lesser General Public License Version 2.1 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/totient".
+
+include "nat/count.ma".
+include "nat/chinese_reminder.ma".
+
+definition totient : nat \to nat \def
+\lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
+
+theorem totient3: totient (S(S(S O))) = (S(S O)).
+reflexivity.
+qed.
+
+theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
+reflexivity.
+qed.
+
+theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
+totient (n*m) = (totient n)*(totient m).
+intro.
+apply nat_case n.
+intro.simplify.intro.reflexivity.
+intros 2.apply nat_case m1.
+rewrite < sym_times.
+rewrite < sym_times (totient O).
+simplify.intro.reflexivity.
+intros.
+unfold totient.
+apply count_times m m2 ? ? ?
+(\lambda b,a. cr_pair (S m) (S m2) a b) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)).
+intros.unfold cr_pair.
+apply le_to_lt_to_lt ? (pred ((S m)*(S m2))).
+unfold min.
+apply le_min_aux_r.
+change with (S (pred ((S m)*(S m2)))) \le ((S m)*(S m2)).
+apply nat_case ((S m)*(S m2)).apply le_n.
+intro.apply le_n.
+intros.
+generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+intro.elim H3.
+apply H4.
+intros.
+generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+intro.elim H3.
+apply H5.
+intros.
+generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
+intro.elim H3.
+apply eqb_elim.
+intro.
+rewrite > eq_to_eqb_true.
+rewrite > eq_to_eqb_true.
+reflexivity.
+rewrite < H4.
\ No newline at end of file
projects / helm.git / commitdiff