proposition: Lemma comp_polyXaddC_K p z : (p \Po ('X + z%:P)) \Po ('X - z%:P) = p.
proof: Proof. have addzK: ('X + z%:P) \Po ('X - z%:P) = 'X. by rewrite raddfD /= comp_polyC comp_polyX subrK. elim/poly_ind: p => [|p c IHp]; first by rewrite !comp_poly0. rewrite comp_poly_MXaddC linearD /= comp_polyC {1}/comp_poly rmorphM /=. by rewrite hornerM_comm /comm_poly -!/(_ \Po _) ?IHp ?addzK ?commr_polyX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)