proposition: Lemma ratMult_inverse : forall r1 r2 (p1 p2 : posnat), r1 == r2 * (RatIntro p1 p2) -> r1 * (RatIntro p2 p1) == r2.
proof: Proof. intuition. rewrite H. rewrite <- (ratMult_1_r r2) at 2. rewrite ratMult_assoc. eapply ratMult_eqRat_compat. intuition. rewrite <- ratMult_num_den. eapply num_dem_same_rat1. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms