cut b \leq r.
apply lt_to_not_le r b H2 Hcut2.
elim Hcut.assumption.
-apply trans_le ? ((q1-q)*b) ?.
+apply trans_le ? ((q1-q)*b).
apply le_times_n.
apply le_SO_minus.exact H6.
rewrite < sym_plus.
rewrite < sym_times.
rewrite > distr_times_minus.
(* ATTENZIONE ALL' ORDINAMENTO DEI GOALS *)
-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.
rewrite > sym_times.
rewrite < H5.
rewrite < sym_times.
cut b \leq r1.
apply lt_to_not_le r1 b H4 Hcut2.
elim Hcut.assumption.
-apply trans_le ? ((q-q1)*b) ?.
+apply trans_le ? ((q-q1)*b).
apply le_times_n.
apply le_SO_minus.exact H6.
rewrite < sym_plus.
apply le_plus_n.
rewrite < sym_times.
rewrite > distr_times_minus.
-rewrite > plus_minus ? ? ? ?.
+rewrite > plus_minus.
rewrite > sym_times.
rewrite < H3.
rewrite < sym_times.
qed.
variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
-\def lt_O_to_injective_times_l.
\ No newline at end of file
+\def lt_O_to_injective_times_l.