proposition: Lemma bisum_shifting : forall u n p, bisum (shiftp u p) (n + p) = bisum u n + sum1 (shiftp u n) (2 * p) .
proof: Proof. intros. induction p. rewrite bisum_eq_compat with _ u _; [| intro; unfold shiftp; inject; simpl Z_of_nat; lia]. simpl. ring_simplify; inject; lia. rewrite <- plus_n_Sm. replace (mult 2 (S p)) with (S (S (2 * p))) by lia. replace (sum1 (shiftp u n) (S (S (2 * p)))) with (sum1 (shiftp u n) (2 * p) + (shiftp u n) (Z_of_nat (S (2 * p))) + (shiftp u n) (Z_of_nat (S (S (2 * p))))) by trivial. repeat rewrite <- Rplus_assoc. rewrite <- IHp; clear IHp. replace (bisum (shiftp u (S p)) (S (n + p))) with (bisum (shiftp u p) (n + p) + (shiftp u n) (Z_of_nat (S (2 * p))) + (shiftp u n) (Z_of_nat (S (S (2 * p))))) ; [trivial | ]. rewrite bisum_shifting_S. unfold shiftp. replace (mult 2 p) with (plus p p) by lia. assert (AP : forall a b c a' b' c', a = a' -> b = b' -> c = c' -> a + b + c = a' + b' + c') by (intros; subst; ring); apply AP; clear AP; trivial; inject; repeat (repeat rewrite inj_S; repeat rewrite inj_plus); lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith