proposition: Lemma compare_trans: forall c x y z, compare x y = c -> compare y z = c -> compare x z = c.
proof: Proof. intros c [x x'] [y y'] [z z']; simpl. case_eq (O.compare x y); case_eq (O.compare y z); intros xy yz; simpl; try rewrite (O.compare_trans _ _ _ _ yz xy); intros; subst; try discriminate; auto. eauto using U.compare_trans. apply O.reflect in yz; subst. rewrite xy. trivial. apply O.reflect in yz; subst. rewrite xy. trivial. apply O.reflect in xy; subst. rewrite yz. trivial. apply O.reflect in xy; subst. rewrite yz. trivial. Qed.
imports: Coq(List) Coq(NArith)