proposition: Lemma maxRat_leRat_same : forall r1 r2 r3, r1 <= r3 -> r2 <= r3 -> maxRat r1 r2 <= r3.
proof: Proof. intuition. unfold maxRat in *. case_eq (bleRat r1 r2); intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms