proposition: Lemma Qcmult_le_mono_pos_l x y z : 0 < z → x ≤ y ↔ z * x ≤ z * y.
proof: Proof. split; auto using Qcmult_le_mono_nonneg_l, Qclt_le_weak. rewrite !Qcle_ngt, !(Qcmult_comm z). intuition auto using Qcmult_lt_compat_r. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)