proposition: Lemma nat_compare_spec: forall i j, compare_spec (i=j) (nat_compare i j).
proof: Proof. induction i; intros [|j]; try (constructor; congruence). simpl. case IHi; constructor; congruence. Qed.
imports: List Eqdep Eqdep_dec