proposition: Lemma neg_odd_not_zero : forall n, 2 * (INR n) - 1 <> 0.
proof: Proof. intros. destruct n. simpl. replace (2 * 0 - 1) with (- 1) by field. apply Ropp_neq_0_compat; apply R1_neq_R0. INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia