proposition: Lemma clean_assoc_aux: forall x a, equal (plus a x) (clean_sum a x) /\ equal (dot a x) (clean_prod a x).
proof: Proof. induction x; simpl; intro a; split; rewrite ?cdot_correct, ?cplus_correct; try rewrite <- (lambda_and_r IHx2); try rewrite <- (lambda_and_l IHx2); try rewrite <- (lambda_and_r IHx1); try rewrite <- (lambda_and_l IHx1); auto. rewrite plus_com; auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)