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'. Qed.
imports: Coq(List) Coq(NArith)