proposition: Lemma uniq_extend_1 m n m' (l : seq V) (mn : m != n) (nm' : n != m') (nl : n \notin l) (Hun : uniq (rcons (m' :: l) m)) : uniq [:: m, n, m' & l].
proof: Proof. move: Hun. rewrite rcons_cons [uniq (m' :: _)]/= rcons_uniq mem_rcons inE /= negb_or -andbA. case/and4P => H1 H2 H3 H4; rewrite !inE !negb_or /= mn /= eq_sym H1 /= H3 /=. by rewrite nm' /= nl /= H2. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext