proposition: Lemma Hpc: SetoidList.compat_op VLst.eq equal fplus.
proof: Proof. intros i j H x y H'; unfold fplus. destruct_tests; rewrite (VLst_to_X_compat H); auto with compat. rewrite <- H'. symmetry; constructor. rewrite H'. constructor. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)