proposition: Theorem ratFraction_ge_1_inv : forall r1 r2, 1 <= r1 * (ratInverse r2) -> r2 <= r1.
proof: Proof. intuition. destruct (eq_Rat_dec r2 0). rewrite e. eapply rat0_le_all. eapply (@leRat_ratMult_same_r (ratInverse r2)). intuition. eapply ratInverse_nz. eauto. rewrite ratMult_comm. rewrite ratInverse_prod_1. intuition. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms