proposition: Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E -> L) x : P x -> c_ x != 0 -> exists2 a, a \in E & \sum_(y | P y) c_ y * y a != 0.
proof: Proof. have [n] := ubnP #|P|; elim: n c_ x P => // n IHn c_ x P lePn Px nz_cx. rewrite ltnS (cardD1x Px) in lePn; move/IHn: lePn => {n IHn}/=IH_P. have [/eqfun_inP c_Px'_0 | ] := boolP [forall (y | P y && (y != x)), c_ y == 0]. exists 1; rewrite ?mem1v // (bigD1 x Px) /= rmorph1 mulr1. by rewrite big1 ?addr0 // => y /c_Px'_0->; rewrite mul0r. case/forall_inPn => y Px'y nz_cy. have [Py /gal_eqP/eqlfun_inP/subvPn[a Ea]] := andP Px'y. rewrite memv_ker !lfun_simp => nz_yxa; pose d_ y := c_ y * (y a - x a). have /IH_P[//|b Eb nz_sumb]: d_ y != 0 by rewrite mulf_neq0. have [sumb_0|] := eqVneq (\sum_(z | P z) c_ z * z b) 0; last by exists b. exists (a * b); first exact: rpredM. rewrite -subr_eq0 -[z in _ - z](mulr0 (x a)) -[in z in _ - z]sumb_0. rewrite mulr_sumr -sumrB (bigD1 x Px) rmorphM /= mulrCA subrr add0r. congr (_ != 0): nz_sumb; apply: eq_bigr => z _. by rewrite mulrCA rmorphM -mulrBr -mulrBl mulrA. 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)