proposition: Lemma tool_nth : forall (s: seq 'I_l) (n:nat) (x: 'I_n) (d: 'I_l), nth (val d) (map val s) x = val (nth d s x).
proof: Proof. elim => [ | hd tl hi] //= n x d. - by rewrite !nth_nil. case: n x => [[] // | n]. rewrite [n.+1]/(1 + n)%nat => x. case: (splitP x) => [j | j -> /=]. - by rewrite [j]ord1 => ->. exact: hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor