proposition: Lemma clean_assoc_correct: forall x, equal x (clean_sum zero (clean0 x)).
proof: Proof. intro. rewrite <- (proj1 (clean_assoc_aux (clean0 x) zero)). rewrite <- clean0_correct. auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)