proposition: Lemma cmp_opp : forall x y, cmp x y = CompOpp (cmp y x).
proof: Proof. induction x; destruct y; simpl; auto. apply BCmp.cmp_opp. rewrite IHx1. destruct (cmp y1 x1); simpl; auto. Qed.
imports: Coq(Relations) CoLoR(VecUtil LogicUtil OrdUtil NatUtil)