proposition: Lemma rat_le_1 : forall n (d : posnat), (n <= d)%nat -> (RatIntro n d) <= 1.
proof: Proof. rattac. inversion H1; clear H1; subst. rewrite Nat.mul_1_r. rewrite Nat.mul_1_l. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms