proposition: Lemma bisum_shifting_S : forall u a b, bisum (shiftp u (S b)) (S a) = bisum (shiftp u b) a + u (Z_of_nat (S (a + b))) + u (Z_of_nat (S (S (a + b)))) .
proof: Proof. intros. induction a. unfold bisum, shiftp. assert (AP : forall a b c a' b' c', a = a' -> b = b' -> c = c' -> a + b + c = c' + a' + b') by (intros; subst; ring); apply AP; clear AP; inject; simpl (0 + b)%nat; simpl (Z_of_nat 1); repeat rewrite inj_S; lia. rewrite bisum_one_step. rewrite IHa; clear IHa. rewrite bisum_one_step. repeat rewrite Rplus_assoc. inject. unfold shiftp. repeat rewrite <- Rplus_assoc. assert (AP : forall a b c d a' b' c' d', a = a' -> b = b' -> c = c' -> d = d' -> a + b + c + d = a' + d' + b' + c') by (intros; subst; ring); apply AP; clear AP; inject; try (simpl (0 + b)%nat; simpl (Z_of_nat 1); repeat rewrite inj_S; lia); repeat rewrite inj_S; rewrite inj_plus; repeat rewrite inj_S; lia. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith