proposition: Lemma leRat_0_eq : forall r, (r <= 0 -> r == 0)%rat.
proof: Proof. intuition. rattac. eapply Nat.le_0_r. unfold natToPosnat, posnatToNat in *. rewrite Nat.mul_1_r in l. rewrite l. destruct p. rewrite Nat.mul_0_l. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms