proposition: Lemma add_incr : forall {tar} `{DS.WF tar} l, tar <T= (tar +++ l).
proof: Proof. intros tar Hwf l; revert tar Hwf. induction l as [ | [x y] l IH]. intros; reflexivity. intros; simpl. transitivity (DS.union tar x y). apply DSUtils.le_union. apply IH. ti_auto. 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(Utils_WF) Coq(Relations) Coq(List)