proposition: Lemma right_prefix : forall x y z:List, ltl x (y ++ z) -> ltl x y \/ (exists y' : List, x = y ++ y' /\ ltl y' z).
proof: Proof. intros x y; generalize x. elim y; simpl. right. exists x0; auto with sets. intros. inversion H0. left; apply (Lt_nil A leA). left; apply (Lt_hd A leA); auto with sets. generalize (H x1 z H3). simple induction 1. left; apply (Lt_tl A leA); auto with sets. simple induction 1. simple induction 1; intros. rewrite H8. right; exists x2; auto with sets. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)