proposition: Lemma compare_sym: forall x y, compare y x = CompOpp (compare x y).
proof: Proof. induction x; intros y; destruct y; simpl; auto. rewrite O.compare_sym. destruct (O.compare a t0); simpl; auto. Qed.
imports: Coq(List) Coq(NArith)