proposition: Lemma sum_distr_left `{ISR: IdemSemiRing}: forall A B C (x: X B A) (f: nat -> X C B), forall i k, sum i k f * x == sum i k (fun u => f u * x).
proof: Proof. exact (@sum_distr_right _ _ _ (@Dual.IdemSemiRing _ _ _ ISR)). Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)