proposition: Lemma match_compOpp : forall x (B:Type) (be bl bg:B), match CompOpp x with Eq => be | Lt => bl | Gt => bg end = match x with Eq => be | Lt => bg | Gt => bl end.
proof: Proof. destruct x;simpl;intros;trivial. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom