proposition: Lemma r_pow_succ: forall r n s1 s2, s1 \in r -> s2 \in r_pow r n -> s1 ++ s2 \in r_pow r (S n).
proof: Proof. intros. simpl. apply accept_app with (s1:=s1) (s2:=s2); auto. Qed.
imports: Coq.micromega.Lia Turing.Util Turing.Lang