proposition: Lemma small_cycTI_NC phi i0 j0 (a0 := '[phi, eta_ i0 j0]) : {in V, forall x, phi x = 0} -> (NC phi < 2 * minn w1 w2)%N -> a0 != 0 -> (forall i j, '[phi, eta_ i j] = (j == j0)%:R * a0) \/ (forall i j, '[phi, eta_ i j] = (i == i0)%:R * a0).
proof: Proof. pose a i j := '[phi, eta_ i j]; pose A := [set ij | a ij.1 ij.2 != 0]. rewrite -[NC phi]/#|A| ltnNge => phiV_0 ubA nz_a0. have{phiV_0} Da i2 j2 i1 j1 : a i1 j1 = a i1 j2 + a i2 j1 - a i2 j2. by rewrite cycTIiso_cfdot_exchange ?addrK. have ubA2: ~~ (w2 + w1 <= #|A| + 2)%N. rewrite addnC addn2 -ltnS (contra _ ubA) //; apply: (@leq_trans _ _.+3). rewrite odd_geq /= ?oddD ?oddW1 ?oddW2 // mul2n -addn_min_max -addnn. by rewrite uphalf_double leq_add2l gtn_min !leq_max !ltnn orbF -neq_ltn. have Za i1 i2 j1 j2 : a i1 j2 == 0 -> a i2 j1 == 0 -> a i1 j1 == 0. have [-> // | /negPf i2'1 /eqP Za12 /eqP Za21] := eqVneq i1 i2. apply: contraR ubA2 => nz_a11. pose L := [set (if a i1 j == 0 then i2 else i1, j) | j : Iirr W2]. pose C := [set (i, if a i j1 == 0 then j2 else j1) | i : Iirr W1]. have [<- <-]: #|L| = w2 /\ #|C| = w1 by rewrite !card_imset // => ? ? []. have <-: #|[set (i1, j1); (i2, j2)]| = 2%N by rewrite cards2 xpair_eqE i2'1. rewrite -cardsUI leq_add ?subset_leq_card //; last first. apply/subsetP=> _ /setIP[/imsetP[j _ ->] /imsetP[i _ []]]. by case: ifP => _ <- ->; rewrite !inE ?Za21 ?(negPf nz_a11) !eqxx ?orbT. apply/subsetP=> ij /setUP[] /imsetP[] => [j | i] _ {ij}->; rewrite inE. by case: ifPn => // /eqP Za1j; rewrite (Da i1 j1) Za21 Za1j !add0r oppr_eq0. by case: ifPn => // /eqP Zai1; rewrite (Da i1 j1) Za12 Zai1 !add0r oppr_eq0. pose L i := [set ij | ij.1 == i] :&: A; pose C j := [set ij | ij.2 == j] :&: A. have{ubA2} ubLC i j: (#|L i| + #|C j| != w2 + w1)%N. apply: contraNneq ubA2 => <-; rewrite addnS leqW // -cardsUI -setIUl -setIIl. rewrite -(card1 (i, j)) leq_add ?subset_leq_card ?subsetIr //. by apply/subsetP=> ij /setIP[]; rewrite !inE. have lbA L1 L2: L1 :&: L2 =i set0 -> (#|L1 :&: A| + #|L2 :&: A| <= #|A|)%N. rewrite -cardsUI -setIUl -setIIl => /setP->. by rewrite set0I cards0 addn0 subset_leq_card ?subsetIr. have oL i1: ~~ [exists j, a i1 j == 0] -> #|L i1| = w2. rewrite negb_exists => /forallP nz_a1. transitivity #|predX (pred1 i1) (Iirr W2)|; last by rewrite cardX card1 mul1n. by apply/eq_card=> ij; rewrite !inE andbT andb_idr // => /eqP->. have oC i1 j1 j2 : a i1 j1 != 0 -> a i1 j2 == 0 -> #|C j1| = w1. move=> nz_a11 /(Za i1)/contra/(_ nz_a11) nz_a1. transitivity #|predX (Iirr W1) (pred1 j1)|; last by rewrite cardX card1 muln1. by apply/eq_card=> ij; rewrite !inE andb_idr // => /eqP->. have [/existsP[j1 Za01] | /oL oL0] := boolP [exists j, a i0 j == 0]. have j0'1 : j1 != j0 by apply: contraTneq Za01 => ->. have oC0: #|C j0| = w1 by apply: oC nz_a0 Za01. suffices Za0 i j: j != j0 -> a i j = 0. left=> i j; rewrite -/(a i j) mulr_natl mulrb; have [->|/Za0//] := altP eqP. by rewrite (Da i0 j1) !(Za0 _ j1) // subr0 add0r. move=> j0'j; apply: contraNeq (ubLC i j0) => nz_aij; rewrite oC0 oL //. apply: contra ubA => /existsP[_ /Za/contra/(_ nz_aij) nz_a_j]. rewrite minnMr geq_min mul2n -addnn -{2}oC0 -(oC i0 j j1) ?lbA // => ij. by rewrite !inE; apply/andP=> [[/eqP-> /idPn]]. suffices Za0 i j: i != i0 -> a i j = 0. right=> i j; rewrite -/(a i j) mulr_natl mulrb; have [->|/Za0//] := altP eqP. have /card_gt0P[i1 i0'i]: (0 < #|predC1 i0|)%N. by rewrite cardC1 nirrW1 -(subnKC w1gt2). by rewrite (Da i1 j0) !(Za0 i1) // subr0 addr0. move=> i0'i; suffices /existsP[j1 Zai1]: [exists j, a i j == 0]. by apply: contraNeq (ubLC i0 j) => /oC/(_ Zai1)->; rewrite oL0. apply: contraR ubA; rewrite minnMr geq_min orbC mul2n -addnn => /oL{1}<-. by rewrite -oL0 lbA // => ij; rewrite !inE; apply/andP=> [[/eqP-> /idPn]]. 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)