proposition: Lemma ratMult_sumList_rel_distrib : forall (A : Set)(ls : list A) f (x : Rat -> Prop) x' a, sumList_rel f ls a -> (forall i v1 v2, f i v1 -> f i v2 -> v1 == v2) -> (forall x1 x2, x x1 -> x x2 -> x1 == x2) -> x x' -> sumList_rel (fun i => ratMult_rel x (f i)) ls (x' * a).
proof: Proof. induction ls; intuition. inversion H; clear H; subst. econstructor. rewrite H3. apply ratMult_0_r. inversion H; clear H; subst. econstructor. eauto. unfold ratMult_rel. intuition. eapply ratMult_eqRat_compat; eauto. rewrite H8. eapply ratMult_distrib. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation