proposition: Lemma leRat_mult : forall n1 n2 d1 d2 (pf1 : d1 > 0) (pf2 : d2 > 0), RatIntro n1 (exist (fun d => d > 0) _ pf1) <= RatIntro n2 (exist (fun d => d > 0) _ pf2) -> (n1 * d2 <= n2 * d1)%nat.
proof: Proof. rattac. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms