proposition: Lemma store_aux_correct n (l : seq A) (j : 'I_n) v (j' : 'I_n) : size l = n -> nth 0%C (store_aux l j v) j' = if j' == j then v else nth 0%C l j'.
proof: Proof. elim: n j j' l; [by case|]; move=> n IH j j'. case=>// h t [Ht]; case j' => {j'}; case; case j => {j}; case=>//= j Hj j' Hj'. rewrite /eqtype.eq_op /= eqSS; rewrite !ltnS in Hj, Hj'. apply (IH (Ordinal Hj) (Ordinal Hj') _ Ht). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms