proposition: Lemma size_nth_store_seqmx0 s i j k x : size (nth [::] (@store_seqmx0 A s j i x) k) = size (nth [::] s k).
proof: Proof. elim: s j k => [|a s IHs] j k; first by case: j. case: j IHs => [|j] IHs //=; case: k IHs => [|k] IHs //=. by rewrite size_store_aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype bigop matrix) CoqEAL(hrel param refinements seqmx seqpoly) Equivalence RelationClasses Morphisms