qed.
theorem times_mod: ∀a,b,c:nat.
O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
#a #b #c #posc #posb
@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))
qed.
theorem times_mod: ∀a,b,c:nat.
O < c → O < b → (a*c) \mod (b*c) = c*(a\mod b).
#a #b #c #posc #posb
@(div_mod_spec_to_eq2 (a*c) (b*c) (a/b) ((a*c) \mod (b*c)) (a/b) (c*(a \mod b)))