proposition: Lemma purely_inseparable_trans M K E : purely_inseparable K M -> purely_inseparable M E -> purely_inseparable K E.
proof: Proof. have insepP := purely_inseparableP => /insepP insepK_M /insepP insepM_E. have insepPe := purely_inseparable_elementP. apply/insepP=> x /insepM_E/insepPe[n charLn /insepK_M/insepPe[m charLm Kxnm]]. by apply/insepPe; exists (n * m)%N; rewrite ?exprM // pnatM charLn charLm. 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)