proposition: Lemma in_classes_empty_below: forall size x, StateSetSet.In x (classes size DS.empty) -> setbelow x (state_of_nat size).
proof: Proof. intros size x H z. rewrite in_classes in H. destruct H as [y Hy H]. rewrite H. rewrite DSUtils.class_of_empty. StateSetProps.set_iff. intro. psubst. num_lia. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)