proposition: Lemma normalP p q (A : 'M_(p, n)) (B :'M_(q, n)) : reflect (forall (u v : 'rV_n), (u <= A)%MS -> (v <= B)%MS -> u _|_ v) (A _|_ B).
proof: Proof. apply: (iffP idP) => AnB. move=> u v uA vB; rewrite (submx_trans uA) // (submx_trans AnB) //. apply/sub_kermxP; have /submxP [w ->] := vB. rewrite trmx_mul map_mxM !mulmxA -[kermx _ *m _ *m _]mulmxA. by rewrite [kermx _ *m _](sub_kermxP _) // mul0mx. apply/rV_subP => u /AnB /(_ _) /sub_kermxP uMv; apply/sub_kermxP. suff: forall m (v : 'rV[R]_m), (forall i, v *m 'e_i ^t theta = 0 :> 'M_1) -> v = 0. apply => i; rewrite !mulmxA -!mulmxA -map_mxM -trmx_mul uMv //. by apply/submxP; exists 'e_i. move=> /= m v Hv; apply: (can_inj (@trmxK _ _ _)). rewrite trmx0; apply/row_matrixP=> i; rewrite row0 rowE. apply: (can_inj (@trmxK _ _ _)); rewrite trmx0 trmx_mul trmxK. by rewrite -(map_delta_mx theta) map_trmx Hv. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)