proposition: Lemma minRat_le_l : forall r1 r2, minRat r1 r2 <= r1.
proof: Proof. unfold minRat in *. intuition. case_eq (bleRat r1 r2); intuition. eapply bleRat_total. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms