proposition: Lemma PaddX_ok : forall P2 P k n l, (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l.
proof: Proof. intro P2. elim (PaddX_ok2 P2); auto. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring