proposition: Lemma repeat_eq_elt x y n l1 l2 : repeat x n = l1 ++ y :: l2 -> x = y /\ repeat x (length l1) = l1 /\ repeat x (length l2) = l2.
proof: Proof. intros Hr; apply repeat_eq_app in Hr as [Hr1 Hr2]; subst. apply repeat_eq_cons in Hr2; intuition. Qed.
imports: PeanoNat