proposition: Lemma repeat_eq_app x n l1 l2 : repeat x n = l1 ++ l2 -> repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
proof: Proof. revert n; induction l1 as [|a l1 IHl1]; simpl; intros n Hr; subst. - repeat split; now rewrite repeat_length. - destruct n; inversion Hr as [ [Heq Hr0] ]; subst. now apply IHl1 in Hr0 as [-> ->]. Qed.
imports: PeanoNat