proposition: Lemma anz_antg : forall n, antg n = anz (Z_of_nat n).
proof: Proof. intro n. unfold antg, anz. destruct n. simpl; field. rewrite pow1_nat. rewrite <- INR_IZR_INZ. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith