proposition: Lemma inj_f : injective f.
proof: Proof. move=> -[x1 x2] -[y1 y2]; rewrite /f /= => H. move: (H) => /(congr1 (@lsubmx A 1 1 n)); rewrite 2!row_mxKl => /rowP/(_ ord0). rewrite !mxE => ->; congr (_, _). by move: H => /(congr1 (@rsubmx A 1 1 n)); rewrite 2!row_mxKr. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext