proposition: Lemma pumping_constant_0_false : forall T (re : reg_exp T), pumping_constant re = 0 -> False.
proof: Proof. intros T re H. assert (Hp1 : pumping_constant re >= 1). { apply pumping_constant_ge_1. } inversion Hp1 as [Hp1'| p Hp1' Hp1'']. - rewrite H in Hp1'. discriminate Hp1'. - rewrite H in Hp1''. discriminate Hp1''. Qed.
imports: Coq(Lia)