proposition: Lemma Qcinv_pos_le_compat : forall q q', 0 < q -> q <= q' -> / q' <= / q.
proof: Proof. intros q q' Hpos Hlt. rewrite <- Qcmult_1_l. change (1 * / q) with (1 / q). rewrite Qcle_shift_div_l. rewrite Qcmult_comm. change (q * / q') with (q / q'). rewrite Qcle_shift_div_r. now rewrite Qcmult_1_l. now apply Qclt_le_trans with q. assumption. Qed.
imports: Qfield Qreduction Qcanon