proposition: Lemma positive_size: 0 < size'.
proof: Proof. assert (H:=build_store_correct). eapply proj1, e_next in H. simpl in H. change 2%positive with (state_of_nat 1) in H. num_lia. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)