proposition: Lemma add_cardinal: forall s s' x, Datatypes.S (StateSetSet.cardinal s) < StateSetSet.cardinal s' -> StateSetSet.cardinal (StateSetSet.add x s) < StateSetSet.cardinal s'.
proof: Proof. intros. destruct (StateSetSetProps.mem_spec x s) as [Hx|Hx]. rewrite StateSetSetProps.Props.add_cardinal_1; auto with lia. rewrite StateSetSetProps.Props.add_cardinal_2; auto. Qed.
imports: ATBR(Utils_WF) ATBR(DisjointSets) ATBR(DKA_Definitions) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties) ATBR(Common)