proposition: Lemma antg_shift_neg_compat : Rseq_shift antg_neg == antg.
proof: Proof. intro n. unfold Rseq_shift. unfold antg. unfold antg_neg. rewrite S_INR. simpl pow. field; split; replace (-2) with (-(2%R)) by reflexivity; replace 2 with (INR 2) by reflexivity; replace 1 with (INR 1) by reflexivity. INR_solve. intro Hinv. rewrite Ropp_mult_distr_l_reverse in Hinv. pose proof (Rplus_opp_r_uniq _ _ Hinv) as H. rewrite Ropp_involutive in H. rewrite <- plus_INR in H. rewrite <- mult_INR in H. generalize dependent H. apply not_INR. lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia