proposition: Lemma maxRat_eqRat_compat : forall r1 r2 r3 r4, r1 == r3 -> r2 == r4 -> maxRat r1 r2 == maxRat r3 r4.
proof: Proof. intuition. unfold maxRat. case_eq (bleRat r1 r2); intuition; case_eq (bleRat r3 r4); intuition. apply bleRat_total in H2. eapply leRat_impl_eqRat; eauto using leRat_trans, eqRat_impl_leRat, eqRat_symm. apply bleRat_total in H1. eapply leRat_impl_eqRat; eauto using leRat_trans, eqRat_impl_leRat, eqRat_symm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms