proposition: Lemma Qcle_shift_div_l : forall q q' q'', 0 < q'' -> (q <= q' / q'' <-> q * q'' <= q').
proof: Proof. intros q q' q'' Hq''. unfold Qcle,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. apply Qlt_le_weak in Hq''. now apply Qmult_le_compat_r. intro Goal. symmetry in Goal. revert Goal. now apply Qlt_not_eq. now apply Qle_shift_div_l. Qed.
imports: Qfield Qreduction Qcanon