proposition: Lemma ratMult_ratDistance_factor_r : forall r1 r2 r3, ratDistance (r1 * r3) (r2 * r3) == (ratDistance r1 r2) * r3.
proof: Proof. intuition. destruct (eq_Rat_dec r3 0). repeat rewrite e. repeat rewrite ratMult_0_r. rewrite <- ratIdentityIndiscernables. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r1 r2); intuition. assert (bleRat (r1 * r3) ( r2 * r3) = true). eapply ratMult_leRat_compat; intuition. rewrite H0. rewrite ratMult_ratSubtract_distrib_r. intuition. case_eq (bleRat (r1 * r3) (r2 * r3)); intuition. eapply leRat_ratMult_same_r in H0. congruence. intuition. rewrite ratMult_ratSubtract_distrib_r. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms