proposition: Lemma not_0_INR : forall n:nat, n <> 0%nat -> INR n <> 0.
proof: Proof. intros [| n'] H. - now exfalso; apply H. - rewrite S_INR; apply Rgt_not_eq. now apply Rplus_le_lt_0_compat with (1 := (pos_INR n')); apply Rlt_0_1. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField