proposition: Lemma rat_ge_1 : forall n (d : posnat), n >= d -> 1 <= RatIntro n d.
proof: Proof. intuition. rattac. inversion H1; clear H1; subst. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms