proposition: Lemma ratDistance_le_max : forall r1 r2 r3 v, r1 <= r2 -> r2 <= r3 -> (ratDistance r2 v) <= (maxRat (ratDistance r1 v) (ratDistance r3 v)).
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r3 v); intuition. assert (r2 <= v). rewrite H0. eauto. rewrite H2. assert (r1 <= v). rewrite H. eauto. rewrite H3. assert ((ratSubtract v r3) <= (ratSubtract v r1)). eapply ratSubtract_leRat_r. eauto using leRat_trans. case_eq (bleRat (ratSubtract v r1) (ratSubtract v r3)); intuition. assert (r1 == r3). assert ((ratSubtract v r1) == (ratSubtract v r3)). eapply leRat_antisymm; eauto. eapply ratSubtract_eq_r; eauto. eapply ratSubtract_leRat_r. rewrite <- H6. trivial. eapply ratSubtract_leRat_r. trivial. eapply bleRat_total in H1. case_eq (bleRat r2 v); intuition. assert (r1 <= v). eauto using leRat_trans. rewrite H3. case_eq (bleRat (ratSubtract v r1) (ratSubtract r3 v)); intuition. eapply leRat_trans. eapply ratSubtract_leRat_r. eapply H. eapply H4. eapply ratSubtract_leRat_r; trivial. apply bleRat_total in H2. case_eq (bleRat r1 v); intuition. case_eq (bleRat (ratSubtract v r1) (ratSubtract r3 v)); intuition. assert (r1 <= v). eauto using leRat_trans. eapply ratSubtract_leRat_l; trivial. apply bleRat_total in H4. eapply leRat_trans. eapply ratSubtract_leRat_l. eapply H0. trivial. assert (bleRat (ratSubtract r1 v) (ratSubtract r3 v) = true). eapply ratSubtract_leRat_l. eauto using leRat_trans. rewrite H4. eapply ratSubtract_leRat_l; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms