proposition: Lemma Qmult_pos_monotone_r : forall a, (0 <= a) -> Qmonotone (Qmult a).
proof: Proof. intros a Ha b c H. do 2 rewrite -> (Qmult_comm a). apply Qmult_le_compat_r; auto with *. Qed.
imports: Coq.QArith.QArith_base CoRN.order.TotalOrder