proposition: Lemma collect_max_label: forall a i acc, NumSet.In i (collect a acc) -> forall e f A, nat_of_num i < max_label (build a e f A) \/ NumSet.In i acc.
proof: Proof. induction a; simpl; intros i acc Hi e f A; auto. eapply IHa1 in Hi as [Hi|Hi]. left. apply Hi. eapply IHa2 in Hi as [Hi|Hi]. left. apply build_max_label, Hi. auto. eapply IHa1 in Hi as [Hi|Hi]. left. apply Hi. eapply IHa2 in Hi as [Hi|Hi]. left. apply build_max_label, Hi. auto. rewrite max_label_add_one. auto. revert Hi. NumSetProps.set_iff. intuition. subst. left. destruct A; simpl. num_simpl. eauto using Nat.le_max_l with arith. 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_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)