proposition: Lemma diag_ok : forall {tarjan} `{DS.WF tarjan} x y l, below x size -> below y size -> diag {{tarjan}} {{tarjan +++ l}} -> diag {{DS.union tarjan x y}} {{DS.union tarjan x y +++ add_lists x y ml l}}.
proof: Proof. intros tar Hwf x y l Hx Hy Hl. intros a v w Hv Hw Ha H. rewrite DS.sameclass_union in H. assert (Hle : tar+++l <T= DS.union tar x y +++ add_lists x y ml l). clear - Hwf. induction ml using num_peano_rec; simpl. apply complete_incr_left. auto using DSUtils.le_union. num_simpl. simpl. rewrite IHn. apply complete_incr_left. apply DSUtils.le_union. destruct H as [H | [[Hv' Hw' ] | [Hw' Hv']]]. eapply (Hl a) in H; auto. eapply (Hl a) in Hv'; auto. eapply (Hl a) in Hw'; auto. apply Hle in Hv'. apply Hle in Hw'. rewrite Hv', Hw'. apply add_lists_sameclass, Ha. eapply (Hl a) in Hv'; auto. eapply (Hl a) in Hw'; auto. apply Hle in Hv'. apply Hle in Hw'. rewrite Hv', Hw'. symmetry. apply add_lists_sameclass, Ha. 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)