proposition: Lemma bisum_mult : forall f g n m, (bisum f n) * (bisum g m) = bisum (fun i => bisum (fun j => f i * g j) m) n.
proof: Proof. induction n. simpl; intro. replace (fun j : Z => f 0%Z * g j) with (zr (Rmult (f 0%Z)) g) by trivial. rewrite bisum_scal_mult; trivial. intros m. simpl bisum. repeat rewrite Rmult_plus_distr_r. rewrite IHn. replace (fun j : Z => f (Zpos (P_of_succ_nat n)) * g j) with (zr (Rmult (f (Zpos (P_of_succ_nat n)))) g) by trivial. replace (fun j : Z => f (Zneg (P_of_succ_nat n)) * g j) with (zr (Rmult (f (Zneg (P_of_succ_nat n)))) g) by trivial. repeat rewrite bisum_scal_mult. trivial. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith