proposition: Lemma reflect: forall x y, compare x y = Eq -> x = y.
proof: Proof. intros [x x'] [y y']. simpl. case_eq (O.compare x y); intro xy; try apply O.reflect in xy; case_eq (U.compare x' y'); intro xy'; try apply U.reflect in xy'; intro; try discriminate; subst; auto. Qed.
imports: Coq(List) Coq(NArith)