proposition: Theorem same_labels_max_label: forall a b, same_labels a b = true -> eNFA.max_label (X_to_eNFA a) = eNFA.max_label (X_to_eNFA b).
proof: Proof. intros. rewrite 2 max_label_X_to_eNFA. cut (forall a b, collect a NumSet.empty [=] collect b NumSet.empty -> max_label (build a 0 1 empty) <= max_label (build b 0 1 empty)). intros H'. apply NumSet.equal_2 in H. apply le_antisym; auto. symmetry in H. auto. clear. intros a b H. apply inf_leq. intros c Hc. apply max_label_collect in Hc as [[d ? Hd]|?]. rewrite H in Hd. eapply collect_max_label in Hd as [Hd|?]. eapply Nat.le_lt_trans. eassumption. unfold statesetelt_of_nat in Hd. rewrite id_nat in Hd. eassumption. NumSetProps.setdec. simpl in *. compute in H0. lia_false. 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)