proposition: Lemma norm_correct: forall x, equal x (norm x).
proof: Proof. intro x; unfold norm, X_to_VLSet. rewrite <- (proj2 (normalize_aux _) _ _ _ (le_n _)). rewrite dot_neutral_left, plus_neutral_left; reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)