proposition: Lemma greatest_nodup_prefix_app : forall m l, nodup l -> greatest_nodup_prefix (l ++ m) = greatest_nodup_prefix_aux (rev l) m.
proof: Proof. intros. assert (rev l = rev l ++ nil). apply app_nil_end. rewrite H0. apply greatest_nodup_prefix_aux_app. exact H. simpl. auto. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)