proposition: Lemma kHomExtend_val : kHomExtend x = y.
proof: Proof. have fX: map_poly f 'X = 'X by rewrite (kHom_poly_id homKf) ?polyOverX. have [Ex | E'x] := boolP (x \in E); last first. by rewrite kHomExtendE Fadjoin_polyX // fX hornerX. have:= fPx_y_0; rewrite (minPoly_XsubC Ex) raddfB /= map_polyC fX root_XsubC /=. by rewrite (kHomExtend_id Ex) => /eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)