proposition: Lemma ratDistance_ratInverse : forall r1 r2, ~ r1 == 0 -> ~ r2 == 0 -> ratDistance (ratInverse r1) (ratInverse r2) == (ratDistance r1 r2) * ratInverse (r1 * r2).
proof: Proof. intuition. rewrite ratInverse_ratMult; intuition. rewrite <- ratMult_ratDistance_factor_r. rewrite (ratMult_comm (ratInverse r1)) at 2. repeat rewrite <- ratMult_assoc. rewrite (ratMult_comm r1). rewrite ratInverse_prod_1; intuition. rewrite ratMult_1_l. rewrite (ratMult_comm r2). rewrite ratInverse_prod_1; intuition. rewrite ratMult_1_l. intuition. eapply ratDistance_comm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms