proposition: Lemma bisumsum_square : forall f n, bisumsum (fun i j => f i * f j) n = bisum f n * bisum f n.
proof: Proof. intros. rewrite bisum_mult. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith