proposition: Lemma sat_zero I X : I X =i [:: 0] <-> I |= zero X.
proof: Proof. rewrite sat_and sat_singles sat_not sat_ex1. split. - move => A. split; first by exists 0. move => [n]. move/sat_succ. move/(_ 0 n) => /=. by case/(_ _ _)/Wrap. - move => [[n A] B] k. rewrite A !inE. suff S : n == 0. apply/idP/idP => /eqP->; by rewrite // eq_sym. destruct n as [|n] => //. exfalso. apply B. exists n. by rewrite (sat_succ (x := n) (y := n.+1)). Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)