proposition: Lemma pos_INR : forall n:nat, 0 <= INR n.
proof: Proof. intros [| n]. - now rewrite INR_0; apply Rle_refl. - now left; apply lt_0_INR, Nat.lt_0_succ. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField