proposition: Lemma Hpt: SetoidList.transpose equal fplus.
proof: Proof. intros i j z. unfold fplus. destruct_tests; auto with compat. rewrite plus_com. auto. rewrite plus_com. auto. rewrite <- plus_assoc, (plus_com (VLst_to_X j)). constructor. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)