apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
assumption.
(* congruent to b *)
cut (a2*m = a1*n - (S O)).
apply lt_to_le.
change with (O + a2*m < a1*n).
apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
assumption.
(* and now the symmetric case; the price to pay for working
in nat instead than Z *)
apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
assumption.
(* congruent to a *)
cut (a2*m = a1*n + (S O)).
apply lt_to_le.
change with (O + a1*n < a2*m).
apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
assumption.
(* proof of the cut *)
rewrite < H2.