proposition: Theorem leRat_num : forall n1 n2 d, le n1 n2 -> leRat (RatIntro n1 d) (RatIntro n2 d).
proof: Proof. rattac. eapply Nat.mul_le_mono; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms