proposition: Lemma pid_mx_inj r n (a b : 'rV[R]_r) : r <= n -> a *m (@pid_mx _ r n r) = b *m (@pid_mx _ r n r) -> a = b.
proof: Proof. move=> Hrn /matrixP Heq. apply/matrixP => x y. move: {Heq}(Heq x (widen_ord Hrn y)). rewrite !mxE (ord1 x){x} (bigID (pred1 y)) /= big_pred1_eq (eq_bigr (fun _ => 0)); last first. move=> i Hiy. rewrite mxE /= (_ : nat_of_ord _ == nat_of_ord _ = false) /=; last first. by move/negbTE : Hiy. by rewrite mulr0. rewrite big_const_seq iter_addr0 (bigID (pred1 y)) /= big_pred1_eq (eq_bigr (fun _ => 0)); last first. move=> i Hiy. rewrite mxE /= (_ : nat_of_ord i == nat_of_ord y = false) /=; last first. by move/negbTE : Hiy. by rewrite mulr0. by rewrite big_const_seq iter_addr0 !addr0 !mxE /= eqxx /= (ltn_ord y) /= 2!mulr1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2