proposition: Lemma xyz_rw_ex: forall (a:ascii) p x y z w, length (x ++ y) <= p -> pow1 a p ++ w = x ++ y ++ z -> exists n, p = length (x ++ y) + n /\ length w + n = length z /\ x = pow1 a (length x) /\ y = pow1 a (length y) /\ z = pow1 a n ++ w.
proof: Proof. intros. apply le_to_plus in H. destruct H as (n, Hlen). exists n. split; auto. rewrite <- Hlen in H0. rewrite app_length in H0. rewrite <- Nat.add_assoc in *. apply pow1_plus_xy in H0. destruct H0 as (Ha, Hb). symmetry in Hb. apply pow1_plus_xy in Hb. destruct Hb as (Hb, Hc). repeat split; auto. subst. rewrite app_length. rewrite pow1_length. auto with *. Qed.
imports: Coq.Strings.Ascii Coq.Lists.List Coq.Strings.Ascii Coq.Arith.PeanoNat Coq.micromega.Lia Turing.Lang Turing.Regex Turing.Util