proposition: Lemma anz_antg_neg : forall n, antg_neg n = anz (- Z_of_nat n).
proof: Proof. intro n. unfold antg_neg, anz. destruct n. simpl; field. rewrite pow1_nat_neg. rewrite Ropp_Ropp_IZR. rewrite <- INR_IZR_INZ. field. rewrite plus_1_S. replace (2 * - (1 + INR n) + 1) with (- (1 + 2 * INR n)) by ring. apply Ropp_neq_0_compat. repeat INR_solve. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith