proposition: Lemma leRat_terms : forall n1 n2 (d1 d2 : posnat), (n1 <= n2)%nat -> (d2 <= d1)%nat -> RatIntro n1 d1 <= RatIntro n2 d2.
proof: Proof. rattac. eapply Nat.mul_le_mono; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms