proposition: Lemma Popp_ok : forall P l, (--P)@l == - P@l.
proof: Proof. induction P as [|? IH1 ??? IH2];simpl;intros. - now rewrite ring_morphism_opp. - rewrite IH1, IH2. now rewrite ring_opp_add, ring_opp_mul_l. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring