proposition: Lemma cmP m1 m2 : reflect (forall i, m1 i = m2 i) (m1 == m2).
proof: Proof. by apply: (iffP eqP) => [->//|eq]; apply/val_inj/fsfunP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path choice finset fintype finfun) mathcomp(tuple bigop ssralg ssrint ssrnum) xfinmap