O \lt m \to m \divides a \to m \divides b \to
(gcd (a/m) (b/m)) = (gcd a b) / m.
intros.
apply (inj_times_r1 m H).
rewrite > (sym_times m ((gcd a b)/m)).
rewrite > (NdivM_times_M_to_N (gcd a b) m)
O \lt m \to m \divides a \to m \divides b \to
(gcd (a/m) (b/m)) = (gcd a b) / m.
intros.
apply (inj_times_r1 m H).
rewrite > (sym_times m ((gcd a b)/m)).
rewrite > (NdivM_times_M_to_N (gcd a b) m)