proposition: Lemma rank_argument (n k : nat) (A B : 'M[int]_(n,k)) : (k > 1)%N -> A^T *m B = \matrix_(i < k,j < k) (i != j : int) -> (k <= n)%N.
proof: Proof. move=> k_gt1 AtB; pose toQ := intr : int -> rat. pose A' := map_mx toQ A; pose B' := map_mx toQ B. suff: A'^T *m B' \in unitmx. by move=> /mxrank_unit rkAtB; have := mulmx_max_rank A'^T B'; rewrite rkAtB. have {A A' B B' toQ n AtB}-> : A'^T *m B' = const_mx 1 - 1%:M. have := congr1 (map_mx toQ) AtB; rewrite map_mxM/= -map_trmx => ->. by apply/matrixP => i j; rewrite !mxE/=; case: eqP. rewrite -(@unitmxZ _ _ (- 1)) ?rpredN// scaleN1r opprB. suff: ~~ root (char_poly (const_mx 1 : 'M_k)) (1 : rat). rewrite /root /char_poly -[_.[_]]/(horner_eval _ _) -det_map_mx/=. rewrite /char_poly_mx map_mxD map_mxN/= !map_const_mx map_scalar_mx/=. by rewrite /horner_eval/= hornerX hornerC. rewrite -eigenvalue_root_char; apply/eigenvalueP => -[v]; rewrite scale1r => v1. have{v1} vE i : v ord0 i = \sum_j v ord0 j. by have /rowP/(_ i) := v1; rewrite !mxE; under eq_bigr do rewrite mxE mulr1. have{vE} vMk i : v ord0 i *+ k.-1 = 0. rewrite -subn1 mulrnBr 1?ltnW// mulr1n -[k as X in _ *+ X]card_ord. by rewrite -sumr_const/= vE -sumrB big1 => // j; rewrite vE subrr. apply/negP; rewrite negbK; apply/eqP/rowP => i; rewrite mxE. by have /eqP := vMk i; rewrite mulrn_eq0 -subn1 subn_eq0 ltn_geF// => /eqP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)