proposition: Lemma PaddCl_ok : forall c P l, (PaddCl c P)@l == [c] + P@l .
proof: Proof. induction P as [|????? IH2]; simpl; intros. - now rewrite ring_morphism_add. - now rewrite IH2, !(ring_add_comm [_]), ring_add_assoc. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring