proposition: Lemma greatest_nodup_prefix_intro: forall l, l = greatest_nodup_prefix l \/ exists x, In x (greatest_nodup_prefix l) /\ exists p, l = greatest_nodup_prefix l ++ x :: p.
proof: Proof. induction l; intros. simpl. intuition. assert (nodup (greatest_nodup_prefix l)). apply greatest_nodup_prefix_correct. case (In_dec eq_dec a (greatest_nodup_prefix l)); intro. right. ded (in_elim_dec eq_dec i). do 3 destruct H0. exists a. assert (nodup (a::x)). simpl. split. exact H1. rewrite H0 in H. ded (nodup_app_elim H). intuition. split. simpl. ded (greatest_nodup_prefix_aux_elim l (a::nil)). destruct H3. rewrite H3. simpl. auto. assert (exists p, l = greatest_nodup_prefix l ++ p). destruct IHl. exists nil. rewrite <- H3. apply app_nil_end. decomp H3. exists (x1::x2). exact H4. decomp H3. rewrite H0 in H4. rewrite H4. assert (a::(x++a::x0)++x1 = (a::x)++a::x0++x1). rewrite app_ass. refl. rewrite H3. clear H3. rewrite (greatest_nodup_prefix_app (a::x0++x1) H2). simpl. case (In_dec eq_dec a (rev x ++ a :: nil)); intros. rewrite distr_rev. simpl. rewrite rev_involutive. exists (x0++x1). refl. absurd (In a (rev x++a::nil)). exact n. apply in_appr. simpl. auto. destruct IHl. left. sym. apply nodup_greatest_nodup_prefix. simpl. rewrite H0. intuition. right. decomp H0. exists x. assert (nodup (a::greatest_nodup_prefix l)). simpl. intuition. assert (a::l = (a::greatest_nodup_prefix l)++x::x0). simpl. rewrite <- H1. refl. rewrite H3. clear H3. rewrite (greatest_nodup_prefix_app (x::x0) H0). simpl. rewrite rev_unit, rev_involutive. case (In_dec eq_dec x (rev (greatest_nodup_prefix l) ++ a :: nil)); intro. split. apply in_cons. exact H2. exists x0. refl. absurd (In x (rev (greatest_nodup_prefix l) ++ a :: nil)). exact n0. apply in_appl. apply in_rev. exact H2. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)