proposition: Lemma is_prefix_correct : forall (A : Type) (A_eq_dec : forall x y : A, {x = y} + {x <> y}) (xs ys : list A), is_prefix A_eq_dec xs ys = true <-> exists zs : list A, xs ++ zs = ys.
proof: Proof. intros. split; intro. - generalize dependent ys; induction xs; intros. + exists ys. intuition. + destruct ys. * inversion H. * apply andb_prop in H as []. fold is_prefix in H0. destruct (A_eq_dec a a0). -- apply IHxs in H0 as []. subst. exists x. cbn. subst. reflexivity. -- discriminate. - inversion H. subst. induction xs. + reflexivity. + cbn. destruct (A_eq_dec a a); intuition. apply IHxs. eauto. Qed.
imports: Coq(Lia Lists.List) Equations(Equations)