proposition: Lemma cycTI_NC_minn (phi : 'CF(G)) : {in V, forall x, phi x = 0} -> (0 < NC phi < 2 * minn w1 w2)%N -> (minn w1 w2 <= NC phi)%N.
proof: Proof. move=> phiV_0 /andP[/card_gt0P[[i0 j0]]]; rewrite inE /= => nz_a0 ubNC. pose L := [seq (i0, j) | j : Iirr W2]; pose C := [seq (i, j0) | i : Iirr W1]. have [oL oC]: #|L| = w2 /\ #|C| = w1 by rewrite !card_image // => i j []. have [Da | Da] := small_cycTI_NC phiV_0 ubNC nz_a0. rewrite geq_min -oC subset_leq_card //. by apply/subsetP=> _ /codomP[i ->]; rewrite !inE /= Da eqxx mul1r. rewrite geq_min orbC -oL subset_leq_card //. by apply/subsetP=> _ /codomP[j ->]; rewrite !inE /= Da eqxx mul1r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)