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. revert c. induction x; intros c y z; destruct y; simpl; intro H; auto; subst; try discriminate H; destruct z; simpl; intro H'; eauto; try discriminate H'. revert H'. case_eq (O.compare a t0); case_eq (O.compare t0 t1); intros Hat0 Ht01 H'; (discriminate H' || (try rewrite <- H')); try rewrite (O.compare_trans _ _ _ _ Ht01 Hat0); eauto. apply O.reflect in Ht01. subst. rewrite Hat0. trivial. apply O.reflect in Ht01. subst. rewrite Hat0. trivial. apply O.reflect in Hat0. subst. rewrite Ht01. trivial. apply O.reflect in Hat0. subst. rewrite Ht01. trivial. Qed.
imports: Coq(List) Coq(NArith)