proposition: Lemma pumping (L : word char -> Prop) : (forall k, exists x y z, k <= size y /\ L (x ++ y ++ z) /\ (forall u v w, y = u ++ v ++ w -> ~~ nilp v -> exists i, L (x ++ u ++ rep v i ++ w ++ z) -> False)) -> ~ inhabited (regular L).
proof: Proof. move => H [[A LA]]. move/(_ #|A|.+1) : H => [x] [y] [z] [size_y [/LA Lxyz]]. move: (pump_dfa Lxyz size_y) => [u] [v] [w] [Hn Hy Hv] /(_ u v w Hy Hn). move => [i]. apply. exact/LA. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)