proposition: Lemma bisum_anz_antg : (sum_f_R0 antg + (sum_f_R0 antg_neg - 1))%Rseq == bisum anz.
proof: Proof. intro n. induction n. compute; field. simpl bisum. rewrite <- IHn. unfold Rseq_minus. unfold Rseq_plus. unfold Rseq_constant. repeat rewrite tech5. repeat rewrite anz_antg_neg. repeat rewrite anz_antg. replace (Zneg (P_of_succ_nat n)) with (- Z_of_nat (S n))%Z by trivial. replace (Zpos (P_of_succ_nat n)) with (Z_of_nat (S n))%Z by trivial. ring. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith