proposition: Lemma nth_change_default: forall (s: seq nat) d d' n, n < size s -> nth d s n = nth d' s n.
proof: Proof. elim => [ | hd tl hi] d d' [ | n] //=. rewrite -[n.+1]add1n -[(size tl).+1]add1n ltn_add2l => h. by apply: 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