proposition: Lemma sat_leq I X x Y y : I X =i [:: x] -> I Y =i [:: y] -> I |= Leq X Y <-> x <= y.
proof: Proof. move => A B. rewrite sat_all1. split. - move/(_ y.+1). rewrite sat_imp. case/(_ _)/Wrap. + by rewrite (sat_succ (x := y) (y := y.+1)). + move/(_ x y.+1). rewrite /= A !inE ltnS. by apply. - move => C n. rewrite sat_imp. rewrite (sat_succ (x := y) (y := n)) // => ->. move => ? ? /=. rewrite A !inE => /eqP-> /eqP->. by rewrite ltnS. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)