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. revert H. case_eq (O.compare a t0); intros H' H; try discriminate. apply O.reflect in H'. apply IHx in H. congruence. Qed.
imports: Coq(List) Coq(NArith)