-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.unfold lt.
-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.
-rewrite > sym_gcd.
-rewrite > gcd_mod.
-apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < H5.
-rewrite > sym_gcd.
-rewrite > gcd_mod.
-apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite > sym_times.
-assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-intro.
-apply eqb_elim.
-intro.apply eqb_elim.
-intro.apply False_ind.
-apply H6.
-apply eq_gcd_times_SO.
-unfold lt.apply le_S_S.apply le_O_n.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < gcd_mod.
-rewrite > H4.
-rewrite > sym_gcd.assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-rewrite < gcd_mod.
-rewrite > H5.
-rewrite > sym_gcd.assumption.
-unfold lt.apply le_S_S.apply le_O_n.
-intro.reflexivity.
-intro.reflexivity.
+apply (nat_case1 n)
+[ apply (nat_case1 m)
+ [ intros.
+ simplify.
+ reflexivity
+ | intros.
+ simplify.
+ reflexivity
+ ]
+| apply (nat_case1 m)
+ [ intros.
+ change in \vdash (? ? ? (? ? %)) with (O).
+ rewrite > (sym_times (S m1) O).
+ rewrite > sym_times in \vdash (? ? ? %).
+ simplify.
+ reflexivity
+ | intros.
+ rewrite > H2 in H.
+ rewrite > H1 in H.
+ apply (sigma_p_times m2 m1 ? ? ?
+ (\lambda b,a. cr_pair (S m2) (S m1) a b)
+ (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
+ [intros.unfold cr_pair.
+ apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
+ [unfold min.
+ apply le_min_aux_r
+ |unfold lt.
+ apply (nat_case ((S m2)*(S m1)))
+ [apply le_n|intro.apply le_n]
+ ]
+ |intros.
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
+ apply H6
+ |intros.
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
+ apply H7
+ |intros.
+ generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+ intro.elim H5.
+ apply eqb_elim
+ [intro.
+ rewrite > eq_to_eqb_true
+ [rewrite > eq_to_eqb_true
+ [reflexivity
+ |rewrite < H6.
+ rewrite > sym_gcd.
+ rewrite > gcd_mod
+ [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
+ [unfold lt.apply le_S_S.apply le_O_n
+ |unfold lt.apply le_S_S.apply le_O_n
+ |assumption
+ ]
+ |unfold lt.apply le_S_S.apply le_O_n
+ ]
+ ]
+ |rewrite < H7.
+ rewrite > sym_gcd.
+ rewrite > gcd_mod
+ [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
+ [unfold lt.apply le_S_S.apply le_O_n
+ |unfold lt.apply le_S_S.apply le_O_n
+ |rewrite > sym_times.assumption
+ ]
+ |unfold lt.apply le_S_S.apply le_O_n
+ ]
+ ]
+ |intro.
+ apply eqb_elim
+ [intro.apply eqb_elim
+ [intro.apply False_ind.
+ apply H8.
+ apply eq_gcd_times_SO
+ [unfold lt.apply le_S_S.apply le_O_n.
+ |unfold lt.apply le_S_S.apply le_O_n.
+ |rewrite < gcd_mod
+ [rewrite > H6.
+ rewrite > sym_gcd.assumption
+ |unfold lt.apply le_S_S.apply le_O_n
+ ]
+ |rewrite < gcd_mod
+ [rewrite > H7.
+ rewrite > sym_gcd.assumption
+ |unfold lt.apply le_S_S.apply le_O_n
+ ]
+ ]
+ |intro.reflexivity
+ ]
+ |intro.reflexivity
+ ]
+ ]
+ ]
+ ]
+ ]