proposition: Lemma Qplus_monotone_l : forall a, Qpos_monotone (fun x => Qpos_plus x a).
proof: Proof. intros a x y Hxy. repeat rewrite Q_Qpos_plus. apply Qplus_le_compat. assumption. apply Qle_refl. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder