proposition: Lemma reflect: forall x y, compare x y = Eq -> x = y.
proof: Proof. induction x; intros y; destruct y; simpl; intro H; auto; try discriminate. apply IHx in H. subst. reflexivity. apply IHx in H. subst. reflexivity. Qed.
imports: Coq(List) Coq(NArith)