proposition: Theorem ratTriangleInequality : forall r1 r2 r3, (ratDistance r1 r2) <= (ratDistance r1 r3) + (ratDistance r3 r2).
proof: Proof. intuition. unfold ratDistance, maxRat, minRat in *. case_eq (bleRat r1 r3); intuition. case_eq (bleRat r3 r2); intuition. assert (bleRat r1 r2 = true). eapply leRat_trans; eauto. rewrite H1. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratAdd_comm. } eapply ratSubtract_partition_leRat; eapply leRat_refl. case_eq (bleRat r1 r2); intuition. apply bleRat_total in H0. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratAdd_comm. } eapply ratSubtract_partition_leRat. eapply ratSubtract_leRat; eauto. intuition. apply bleRat_total in H1. apply bleRat_total in H0. eapply ratSubtract_partition_leRat. rewrite ratSubtract_0. eapply rat0_le_all. eapply leRat_refl. eapply ratSubtract_leRat; intuition. apply bleRat_total in H. case_eq (bleRat r1 r2); intuition. assert (bleRat r3 r2 = true). eapply leRat_trans; eauto. rewrite H1. apply ratAdd_any_leRat_r. eapply ratAdd_eq_impl_leRat_r. eapply ratSubtract_partition; eauto. apply bleRat_total in H0. case_eq (bleRat r3 r2); intuition. apply ratAdd_any_leRat_l. eapply ratAdd_eq_impl_leRat_r. eapply ratSubtract_partition; eauto. apply bleRat_total in H1. eapply eqRat_impl_leRat. rewrite ratAdd_comm. eapply ratSubtract_partition; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms