proposition: Lemma rat_le_1_if : forall n d, RatIntro n d <= 1 -> (n <= d)%nat.
proof: Proof. intuition. unfold leRat, bleRat, ratCD, rat1 in *. unfold natToPosnat, posnatToNat in *. destruct d. rewrite Nat.mul_1_r in H. rewrite Nat.mul_1_l in H. destruct (le_gt_dec n x). lia. discriminate. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms