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_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 > assoc_times.
rewrite < div_mod.
reflexivity.
-rewrite > times_n_O O.
+rewrite > (times_n_O O).
apply lt_times.
assumption.assumption.assumption.
qed.