proposition: Lemma tails_are_shorter {A} (y x: L A): In x (tails y) → length x <= length y.
proof: Proof. Proof with auto. induction y; simpl. intros [[] | ?]; intuition. intros [[] | C]... Qed.
imports: Coq.Unicode.Utf8 Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation