proposition: Lemma pumping_constant_neq_0: forall re, pumping_constant re <> 0.
proof: Proof. intros re H. induction re; simpl in H; try (inversion H; fail). - apply Plus.plus_is_O in H. destruct H; auto. - apply Plus.plus_is_O in H. destruct H. auto. - auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang