proposition: Lemma extendDerivationP : separable_element K x -> Derivation <<K; x>> (extendDerivation K).
proof: Proof. move=> sep; apply/allrelP=> u v /vbasis_mem Hu /vbasis_mem Hv; apply/eqP. rewrite -(Fadjoin_poly_eq Hu) -(Fadjoin_poly_eq Hv) -hornerM. rewrite !{1}extendDerivation_horner ?{1}rpredM ?Fadjoin_polyOver //. rewrite (Derivation_mul_poly derD) ?Fadjoin_polyOver //. rewrite derivM !{1}hornerD !{1}hornerM !{1}mulrDl !{1}mulrDr -!addrA. congr (_ + _); rewrite [Dx K]lock -!{1}mulrA !{1}addrA; congr (_ + _). by rewrite addrC; congr (_ * _ + _); rewrite mulrC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)