proposition: Lemma sat_succ I X x Y y : I X =i [:: x] -> I Y =i [:: y] -> I |= succ X Y <-> y = x.+1.
proof: Proof. move => A B. rewrite sat_and sat_not sat_ex1 nat_succ. split => [[C D]|[C D]]. - split; first apply C; rewrite ?A ?B ?mem_head //. apply: impliesPn D; constructor => [[k [k1 k2]]]. exists k. rewrite sat_and /=; split => ? ?; by rewrite ?A ?B => /seq1P-> /seq1P->. - split. move => ? ? ; by rewrite ?A ?B => /seq1P-> /seq1P->. apply: impliesPn D; constructor => [[k] /sat_and [k1 k2]]. exists k. split; [apply k1|apply k2]; by rewrite /= ?A ?B ?mem_head. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)