proposition: Lemma r_star_r_char_in_inv: forall w c, w \in r_star (r_char c) -> exists n, w = pow1 c n.
proof: Proof. intros. apply r_star_to_pow in H. destruct H as (n, Hr). exists n. apply r_pow_char_in_inv in Hr. assumption. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang