proposition: Lemma Is_zero t : is_zero t = true -> t = zero.
proof: Proof. destruct t; simpl; intuition discriminate. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)