proposition: Theorem fold_add_prod : forall (A B : Set)(lsb : list B)(lsa : list A)(fa : A -> Rat)(fb : B -> Rat) initB, fold_left (fun (a : Rat) (b : A) => a + fa b) lsa 0 * fold_left (fun (a : Rat) (b : B) => a + fb b) lsb initB == fold_left (fun (a : Rat) (b : A) => a + fa b * fold_left (fun (a0 : Rat) (b0 : B) => a0 + fb b0) lsb initB) lsa 0.
proof: Proof. induction lsb; intuition idtac; simpl in *. symmetry. rewrite <- fold_add_factor_constant_r. eapply fold_add_eqRat_compat. intuition idtac. eapply ratAdd_eqRat_compat; intuition idtac. reflexivity. rewrite ratMult_0_l. reflexivity. rewrite fold_add_init. rewrite ratMult_distrib. rewrite IHlsb. rewrite <- fold_add_factor_constant_r. rewrite fold_add_eq. eapply fold_add_body_eq. rewrite ratMult_0_l. symmetry. apply ratAdd_0_r. intros. rewrite fold_add_init. rewrite ratMult_distrib. reflexivity. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation