proposition: Lemma bounded_delta_set: forall a p, setbelow (delta_set a p) size.
proof: Proof. intros. unfold delta_set. apply StateSetProps.Props.fold_rec_nodep. intros x Hx. StateSetProps.setdec. intros x i Hx IH y Hy. apply StateSet.union_1 in Hy as [Hy|Hy]; auto. apply HA in Hy. exact Hy. 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)