proposition: Lemma mx_butterfly U V W modU modV modW : ~~ (U == V)%MS -> max_submod U W -> max_submod V W -> let modUV := capmx_module modU modV in max_submod (U :&: V)%MS U /\ mx_rsim (@section_repr V W modV modW) (@section_repr _ U modUV modU).
proof: Proof. move=> neUV maxU maxV modUV; have{neUV maxU} defW: (U + V :=: W)%MS. wlog{neUV modUV} ltUV: U V modU modV maxU maxV / ~~ (V <= U)%MS. by case/nandP: neUV => ?; first rewrite addsmxC; apply. apply/eqmxP/idPn=> neUVW; case: maxU => ltUW; case/(_ (U + V)%MS). rewrite addsmx_module // ltmxE ltmxEneq neUVW addsmxSl !addsmx_sub. by have [ltVW _] := maxV; rewrite submx_refl andbT ltUV !ltmxW. have sUV_U := capmxSl U V; have sVW: (V <= W)%MS by rewrite -defW addsmxSr. set goal := mx_rsim _ _; suffices{maxV} simUV: goal. split=> //; apply/(max_submodP modUV modU sUV_U). by apply: mx_rsim_irr simUV _; apply/max_submodP. apply: {goal}mx_rsim_sym. by apply: mx_rsim_trans (mx_second_rsim modU modV) _; apply: section_eqmx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)