proposition: Theorem ratFraction_le_1 : forall r1 r2, r1 <= r2 -> r1 * (ratInverse r2) <= 1.
proof: Proof. intuition. unfold ratInverse. destruct r2. destruct n. rewrite H. rewrite rat_num_0. rewrite ratMult_0_l. eapply rat0_le_all. rewrite H. rewrite <- ratMult_num_den. eapply rat_le_1. unfold posnatMult, natToPosnat, posnatToNat. destruct p. rewrite Nat.mul_comm. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms