proposition: Lemma eqRat_flip : forall (p1 p2 p3 p4 : posnat), RatIntro p1 p2 == RatIntro p3 p4 -> RatIntro p2 p1 == RatIntro p4 p3.
proof: Proof. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms