From b3f74fab711510628cff64aff3e48e73cc9f6e09 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Nov 2005 11:25:00 +0000 Subject: [PATCH] () around tactic terms --- helm/matita/library/nat/chinese_reminder.ma | 104 ++++++++++---------- helm/matita/library/nat/congruence.ma | 6 +- helm/matita/library/nat/count.ma | 96 +++++++++--------- helm/matita/library/nat/gcd.ma | 2 +- helm/matita/library/nat/minus.ma | 4 +- helm/matita/library/nat/totient.ma | 16 +-- 6 files changed, 114 insertions(+), 114 deletions(-) diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma index 748b06632..f14f16d27 100644 --- a/helm/matita/library/nat/chinese_reminder.ma +++ b/helm/matita/library/nat/chinese_reminder.ma @@ -22,15 +22,15 @@ 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). +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). +apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)). split. (* congruent to a *) -cut a1*n = a2*m + (S O). +cut (a1*n = a2*m + (S O)). rewrite > assoc_times. rewrite > Hcut1. -rewrite < sym_plus ? (a2*m). +rewrite < (sym_plus ? (a2*m)). rewrite > distr_times_plus. rewrite < times_n_SO. rewrite > assoc_plus. @@ -39,12 +39,12 @@ 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). +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 (trans_le ? ((a+b*m)*a2)). apply le_times_l. -apply trans_le ? (b*m). +apply (trans_le ? (b*m)). rewrite > times_n_SO in \vdash (? % ?). apply le_times_r.assumption. apply le_plus_n. @@ -56,8 +56,8 @@ 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. +cut (a2*m = a1*n - (S O)). +rewrite > (assoc_times b a2). rewrite > Hcut1. rewrite > distr_times_minus. rewrite < assoc_times. @@ -65,16 +65,16 @@ 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). +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). +apply (trans_le ? (a1*n - a2*m)). rewrite > H5.apply le_n. -apply le_minus_m ? (a2*m). +apply (le_minus_m ? (a2*m)). apply le_times_l. apply le_times_l. -apply trans_le ? (b*m). +apply (trans_le ? (b*m)). rewrite > times_n_SO in \vdash (? % ?). apply le_times_r.assumption. apply le_plus_n. @@ -88,11 +88,11 @@ 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). +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. +cut (a1*n = a2*m - (S O)). +rewrite > (assoc_times a a1). rewrite > Hcut1. rewrite > distr_times_minus. rewrite < assoc_times. @@ -100,16 +100,16 @@ 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). +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). +apply (trans_le ? (a2*m - a1*n)). rewrite > H5.apply le_n. -apply le_minus_m ? (a1*n). +apply (le_minus_m ? (a1*n)). rewrite > assoc_times.rewrite > assoc_times. apply le_times_l. -apply trans_le ? (a*n). +apply (trans_le ? (a*n)). rewrite > times_n_SO in \vdash (? % ?). apply le_times_r.assumption. apply le_plus_n. @@ -122,10 +122,10 @@ apply lt_minus_to_plus. rewrite > H5.simplify.apply le_n. assumption. (* congruent to a *) -cut a2*m = a1*n + (S O). +cut (a2*m = a1*n + (S O)). rewrite > assoc_times. rewrite > Hcut1. -rewrite > sym_plus (a1*n). +rewrite > (sym_plus (a1*n)). rewrite > distr_times_plus. rewrite < times_n_SO. rewrite < assoc_times. @@ -134,12 +134,12 @@ 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). +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 (trans_le ? ((b+a*n)*a1)). apply le_times_l. -apply trans_le ? (a*n). +apply (trans_le ? (a*n)). rewrite > times_n_SO in \vdash (? % ?). apply le_times_r. assumption. @@ -160,25 +160,25 @@ 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. +intros.elim (and_congruent_congruent m n a b). elim H3. -apply ex_intro ? ? (a1 \mod (m*n)). +apply (ex_intro ? ? (a1 \mod (m*n))). split.split. -apply transitive_congruent m ? a1. +apply (transitive_congruent m ? a1). unfold congruent. apply sym_eq. -change with congruent a1 (a1 \mod (m*n)) m. +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. +apply (transitive_congruent n ? a1). unfold congruent. apply sym_eq. -change with congruent a1 (a1 \mod (m*n)) n. +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. +rewrite > (times_n_O O). apply lt_times.assumption.assumption. assumption.assumption.assumption. qed. @@ -209,43 +209,43 @@ 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. +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. +(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. +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. +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. +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. +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. +rewrite < (lt_to_eq_mod b n).assumption. assumption. -rewrite < lt_to_eq_mod a m.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. +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 diff --git a/helm/matita/library/nat/congruence.ma b/helm/matita/library/nat/congruence.ma index 6bc2b6f68..af744cf34 100644 --- a/helm/matita/library/nat/congruence.ma +++ b/helm/matita/library/nat/congruence.ma @@ -54,8 +54,8 @@ qed. theorem mod_times_mod : \forall n,m,p:nat. O

assoc_times. rewrite < div_mod. reflexivity. -rewrite > times_n_O O. +rewrite > (times_n_O O). apply lt_times. assumption.assumption.assumption. qed. diff --git a/helm/matita/library/nat/count.ma b/helm/matita/library/nat/count.ma index b1cb31cf3..5ebc08b6c 100644 --- a/helm/matita/library/nat/count.ma +++ b/helm/matita/library/nat/count.ma @@ -24,9 +24,9 @@ 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 (g (S (n1+m)))). +rewrite > (sym_plus (g (S (n1+m)))). +rewrite > (assoc_plus (sigma n1 f m)). rewrite < assoc_plus. reflexivity. qed. @@ -35,16 +35,16 @@ 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. +rewrite < (sym_plus n m).reflexivity. simplify. rewrite > assoc_plus in \vdash (? ? ? %). rewrite < H. simplify. rewrite < plus_n_Sm. -rewrite > sym_plus n. +rewrite > (sym_plus n). rewrite > assoc_plus. -rewrite < sym_plus m. -rewrite < assoc_plus n1. +rewrite < (sym_plus m). +rewrite < (assoc_plus n1). reflexivity. qed. @@ -57,10 +57,10 @@ rewrite > assoc_plus in \vdash (? ? ? %). rewrite < H. rewrite < plus_n_Sm. rewrite < plus_n_Sm.simplify. -rewrite < sym_plus n. +rewrite < (sym_plus n). rewrite > assoc_plus. -rewrite < sym_plus m. -rewrite < assoc_plus n. +rewrite < (sym_plus m). +rewrite < (assoc_plus n). reflexivity. qed. @@ -71,12 +71,12 @@ 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. +(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)). +rewrite > (S_pred ((S n1)*(S m))). apply sigma_plus1. simplify.apply le_S_S.apply le_O_n. qed. @@ -123,16 +123,16 @@ theorem count_times:\forall n,m:nat. (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 > (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 ? ? +apply (trans_eq ? ? (sigma n (\lambda a. - sigma m (\lambda b.(bool_to_nat (f2 b))*(bool_to_nat (f1 a))) O) O). + 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 > (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. @@ -145,14 +145,14 @@ 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 ? ? +apply (trans_eq ? ? (sigma n (\lambda n.((bool_to_nat (f1 n)) * -(sigma m (\lambda n.bool_to_nat (f2 n)) O))) O). +(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). +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. @@ -168,9 +168,9 @@ 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 (? ? %). +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. @@ -179,44 +179,44 @@ rewrite > S_pred in \vdash (? ? %). apply le_S_S. rewrite > plus_n_O in \vdash (? ? %). rewrite > sym_times. assumption. -rewrite > times_n_O O. +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. +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 (? ? ? (? % ?)). +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 (? ? %). +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 (? ? %). +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. @@ -226,18 +226,18 @@ 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. +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. +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. +apply (not_le_Sn_O m1 H4). qed. diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index eb2043c98..792629aaa 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -447,7 +447,7 @@ divides (gcd n (m \mod n)) (gcd m n) . intros. apply divides_d_gcd. apply divides_gcd_n. -apply divides_mod_to_divides ? ? n. +apply (divides_mod_to_divides ? ? n). assumption. apply divides_gcd_m. apply divides_gcd_n. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index 1ee70bd39..00a90acd8 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -227,9 +227,9 @@ 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)). +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 False_ind.apply (not_le_Sn_O n H). simplify.intros. apply le_S_S. rewrite < plus_n_Sm. diff --git a/helm/matita/library/nat/totient.ma b/helm/matita/library/nat/totient.ma index 7fc8d95ee..df863fa04 100644 --- a/helm/matita/library/nat/totient.ma +++ b/helm/matita/library/nat/totient.ma @@ -31,22 +31,22 @@ 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. +apply (nat_case n). intro.simplify.intro.reflexivity. -intros 2.apply nat_case m1. +intros 2.apply (nat_case m1). rewrite < sym_times. -rewrite < sym_times (totient O). +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)). +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))). +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. +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). -- 2.39.2