proposition: Lemma leRat_ratMult_same_r : forall r1 r2 r3, (~r1 == 0) -> r2 * r1 <= r3 * r1 -> r2 <= r3.
proof: Proof. intuition. rewrite <- ratMult_1_r. erewrite <- (ratInverse_prod_1 H). rewrite (ratMult_comm (ratInverse r1)). rewrite <- ratMult_assoc. eapply leRat_trans. eapply ratMult_leRat_compat. eapply H0. eapply leRat_refl. rewrite ratMult_assoc. rewrite (ratMult_comm r1). rewrite ratInverse_prod_1. rewrite ratMult_1_r. intuition. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms