proposition: Lemma nat_succ x y : y = x.+1 <-> x < y /\ ~ exists k, x < k /\ k < y.
proof: Proof. split. - move => ->. rewrite leqnn. split=>//. move => [k] [A B]. move:(leq_trans A B). by rewrite ltnn. - move => [A B]. apply/eqP. rewrite eqn_leq leqNgt A andbT. apply/negP. apply: impliesPn B. constructor. exists x.+1. by rewrite leqnn H. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages dfa nfa regexp)