proposition: Lemma compare_sym: forall x y, compare y x = CompOpp (compare x y).
proof: Proof. intros [x x'] [y y']; simpl. rewrite O.compare_sym, U.compare_sym. destruct (O.compare x y); reflexivity. Qed.
imports: Coq(List) Coq(NArith)