proposition: Lemma mxnonsimpleP U : U != 0 -> reflect (mxnonsimple rG U) (mxnonsimple_sat U).
proof: Proof. rewrite /mxnonsimple_sat {1}/mxnonsimple_form; set Vt := vec_mx _ => /= nzU. pose nsim V := [&& mxmodule rG V, (V <= U)%MS, V != 0 & \rank V < \rank U]. set nsimUt := (_ /\ _)%T; have: qf_form nsimUt. by rewrite /= mxmodule_form_qf !mxrank_form_qf !submx_form_qf. move/GRing.qf_evalP; set qev := @GRing.qf_eval _ => qevP. have qev_nsim u: qev (row_env [:: u]) nsimUt = nsim n (vec_mx u). rewrite /nsim -mxrank_eq0 /qev /= eval_mxmodule eval_mxrank. rewrite !eval_submx eval_mx_term eval_vec_mx eval_row_var /=. do 2!bool_congr; apply: andb_id2l => sUV. by rewrite ltn_neqAle andbC !mxrank_leqif_sup. have n2gt0: n ^ 2 > 0. by move: nzU; rewrite muln_gt0 -mxrank_eq0 unlock; case: posnP (U) => // ->. apply: (iffP satP) => [|[V nsimV]]. by case/Exists_rowP=> // v; move/qevP; rewrite qev_nsim; exists (vec_mx v). apply/Exists_rowP=> //; exists (mxvec V); apply/qevP. by rewrite qev_nsim mxvecK. 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)