proposition: Lemma Qcinv_le_1 : forall q, 0 < q -> (/ q <= 1 <-> 1 <= q).
proof: Proof. intros q Hq. rewrite <- (Qcmult_1_l (/ q)). setoid_rewrite <- (Qcmult_1_l q) at 2. change (1 * / q) with (1 / q). now apply Qcle_shift_div_r. Qed.
imports: Qfield Qreduction Qcanon