rewrite > sym_gcd.
rewrite > gcd_mod.
apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
assumption.
-simplify.apply le_S_S.apply le_O_n.
+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)).
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
rewrite > sym_times.
assumption.
-simplify.apply le_S_S.apply le_O_n.
+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.
-simplify.apply le_S_S.apply le_O_n.
-simplify.apply le_S_S.apply le_O_n.
+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.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
rewrite < gcd_mod.
rewrite > H5.
rewrite > sym_gcd.assumption.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
intro.reflexivity.
intro.reflexivity.
qed.
\ No newline at end of file