proposition: Lemma rel_sumList_factor_r : forall (A : Set) (f : A -> Rat) (ls : list A) c rel, RatRel rel -> rel (sumList ls (fun a => (f a) * c)) ((sumList ls f) * c).
proof: Proof. induction ls; intuition; simpl in *. unfold sumList; simpl. eapply refl. symmetry. eapply ratMult_0_l. eapply trans. eapply refl. eapply sumList_cons. eapply trans. 2:{ eapply refl. symmetry. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply sumList_cons. eapply eqRat_refl. eapply ratMult_distrib_r. } eapply add_proper. eapply refl. intuition. eapply IHls; intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia Coq.Classes.RelationClasses Coq.Classes.Morphisms