+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.
+qed.
\ No newline at end of file