proposition: Lemma list_ecompare_app u v u' v' : (forall x y, List.In x u' -> List.In y v -> cmp y x = Gt) -> (forall x y, List.In x u -> List.In y v' -> cmp x y = Lt) -> list_ecompare (u++v) (u'++v') = match list_ecompare u u' with | (Eq,_) => list_ecompare v v' | (c,Early) => (c,Early) | (Lt,EOL) => if v then (Lt,EOL) else (Gt,Early) | (Gt,EOL) => if v' then (Gt,EOL) else (Lt,Early) end.
proof: Proof. revert u'. induction u; destruct u'; intros GT LT; cbn; auto. - destruct v; simpl in *; auto. rewrite GT; auto. - destruct v'; simpl in *; auto. rewrite LT; auto. - case cmp; intuition (auto with datatypes). Qed.
imports: Coq(List)