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: List Relation_Operators Operators_Properties Transitive_Closure