proposition: Lemma Qclt_shift_div_l : forall q q' q'', 0 < q'' -> (q < q' / q'' <-> q * q'' < q').
proof: Proof. intros q q' q'' Hq''. unfold Qclt,Qcdiv,Qcmult,Qcinv in *. repeat rewrite Q2Qc_correct in *. change (q < q' * / q'')%Q with (q < q' / q'')%Q. split. intro. rewrite <- (Qmult_div_r q' q''). setoid_rewrite Qmult_comm at 2. now apply Qmult_lt_compat_r. intro Goal. symmetry in Goal. revert Goal. now apply Qlt_not_eq. now apply Qlt_shift_div_l. Qed.
imports: Qfield Qreduction Qcanon