proposition: Lemma coord0 i v : coord [tuple 0] i v = 0.
proof: Proof. rewrite unlock /pinvmx rank_rV; case: negP => [[] | _]. by apply/eqP/rowP=> j; rewrite !mxE (tnth_nth 0) /= linear0 mxE. by rewrite pid_mx_0 !(mulmx0, mul0mx) mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)