proposition: Lemma list_compare_weak_spec: forall h k, compare_weak_spec h k (list_compare compare h k).
proof: Proof. induction h as [|u h IHh]; destruct k as [|v k]; simpl; try constructor. case (Hcompare a a0 ); try constructor. case (Hcompare u v ); try constructor. case (IHh k); intros; constructor. Defined.
imports: Coq(Arith NArith List RelationClasses)