proposition: Lemma sat_part X I k : I X =i [:: k] -> I |= part X <-> forall n, n <= k -> exists! q:A, n \in I (rank q).
proof: Proof. move => H0. split. - move => H1 m Hm. move/sat_all1 : H1 => /(_ m) /sat_imp. case/(_ _)/Wrap. + rewrite sat_leq ; first apply Hm; done. + case/sat_orE => q _ /sat_and [/= /sub1P q1 /sat_bigand q2]. exists q; split => // q' B. apply/eqP. apply/negPn/negP => C. apply: (q2 q'); by [rewrite mem_enum inE|apply/sub1P]. - move => H1. apply/sat_all1 => m. rewrite sat_imp => /sat_leq H2. have/H1 {H2} : m <= k by apply: H2. case => q [q1 q2]. apply: (sat_orI (x := q)); first by rewrite mem_enum. rewrite sat_and; split; first by move => ? /seq1P ->. apply/sat_bigand => q'. rewrite mem_enum inE => qq' /sub1P /q2 ?. subst. by rewrite eqxx in qq'. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)