proposition: Lemma maxRat_comm : forall r1 r2, maxRat r1 r2 == maxRat r2 r1.
proof: Proof. intuition. unfold maxRat. case_eq (bleRat r1 r2); intuition. case_eq (bleRat r2 r1); intuition. eapply leRat_impl_eqRat; trivial. apply bleRat_total in H. rewrite H. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms