proposition: Theorem leRat_trans : forall r1 r2 r3, leRat r1 r2 -> leRat r2 r3 -> leRat r1 r3.
proof: Proof. rattac. eapply (@mult_le_compat_r_iff x1); trivial. rewrite <- Nat.mul_assoc. rewrite (Nat.mul_comm x). rewrite Nat.mul_assoc. eapply Nat.le_trans. eapply Nat.mul_le_mono. eapply l. eauto. repeat rewrite <- Nat.mul_assoc. repeat rewrite (Nat.mul_comm x0). repeat rewrite Nat.mul_assoc. eapply Nat.mul_le_mono; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia