proposition: Lemma ratAdd_2_ratMax : forall r1 r2, (r1 + r2 <= 2 / 1 * (maxRat r1 r2))%rat.
proof: Proof. intuition. unfold maxRat. case_eq (bleRat r1 r2); intuition. eapply leRat_trans. eapply ratAdd_leRat_compat. eapply H. eapply leRat_refl. rewrite ratMult_2. rewrite ratMult_comm. intuition. apply bleRat_total in H. eapply leRat_trans. eapply ratAdd_leRat_compat. eapply leRat_refl. eapply H. rewrite ratMult_2. rewrite ratMult_comm. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms