proposition: Lemma deg2_poly_root2 : root p r2.
proof: Proof. rewrite /r2 -[2]mulr1 -[X in 2 * X]a1. by apply: deg2_poly_root2; rewrite // -/a a1 mulr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)