proposition: Lemma cplus_correct: forall x a, equal (cplus a x) (plus a x).
proof: Proof. intros. unfold cplus. destruct_tests; auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)