proposition: Fact add_polyN : left_inverse 0%:P opp_poly (@add_poly _).
proof: Proof. move=> p; apply/polyP=> i. by rewrite coef_add_poly coef_opp_poly coefC if_same addNr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)