proposition: Lemma ratDistance_le_max_triv : forall r1 r2, ratDistance r1 r2 <= maxRat r1 r2.
proof: Proof. intuition. eapply leRat_trans. eapply ratDistance_le_max. eapply rat0_le_all. eapply (@ratAdd_any_leRat_l r1 r2). eapply leRat_refl. eapply leRat_trans. eapply eqRat_impl_leRat. eapply maxRat_eqRat_compat. eapply ratDistance_from_0. eapply eqRat_trans. eapply ratDistance_eqRat_compat. eapply eqRat_refl. eapply ratAdd_0_l. rewrite ratDistance_add_same_r. rewrite ratDistance_comm. eapply ratDistance_from_0. rewrite maxRat_comm. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms