proposition: Lemma below0_empty p: setbelow p (num_of_nat 0) -> StateSet.Equal p StateSet.empty.
proof: Proof. intro H. apply StateSetProps.Props.empty_is_empty_1. rewrite StateSetProps.Props.elements_Empty. remember (StateSet.elements p) as l. destruct l as [|i l]. trivial. specialize (H i). apply apply in H. exfalso. clear - H. num_lia. rewrite StateSetProps.Facts.elements_iff. rewrite <- Heql. auto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)