proposition: Lemma ratCD_comm : forall r1 r2 n1 n2 d n1' n2' d', ratCD r1 r2 = (n1, n2, d) -> ratCD r2 r1 = (n1', n2', d') -> n1 = n2' /\ n1' = n2 /\ (posnatEq d d').
proof: Proof. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia