proposition: Theorem le_ratHalf_0 : forall r, r <= (ratHalf r) -> r == 0.
proof: Proof. intuition. unfold ratHalf in *. rattac. unfold posnatMult in *. destruct p. unfold natToPosnat in *. unfold posnatToNat in *. rewrite Nat.mul_1_r in *. rewrite (Nat.mul_comm x) in l. rewrite Nat.mul_assoc in *. assert (n * 2 <= n)%nat. lia. lia. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms