proposition: Lemma list_ecompare_eq_app u v u' v' b : list_ecompare u u' = (Eq,b) -> list_ecompare (u++v) (u'++v') = list_ecompare v v'.
proof: Proof. revert u'; induction u; destruct u'; simpl; try easy. destruct cmp; now auto. Qed.
imports: Coq(List)