-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))).