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