proposition: Lemma mmap1U h i : mmap1 h U_(i) = h i.
proof: Proof. pose inj j := insubd i j; rewrite /mmap1. pose F j := h (inj j) ^+ U_(i)%MM (inj j). have FE j: j < n -> F j = (h (inj j)) ^+ (i == j :> nat). move=> lt_jn; rewrite /F /inj /insubd insubT /=. by rewrite mnm1E -val_eqE. rewrite (eq_bigr (F \o val)) //; last first. by move=> j _ /=; rewrite FE // mnm1E /inj /insubd valK. have ->: n = (i.+1 + (n - i.+1))%N by rewrite subnKC. rewrite big_split_ord /= [X in _*X]big1 ?mulr1; last first. case=> j /= lt_nBSi _; rewrite FE -?ltn_subRL //. case: (_ =P _); last by rewrite expr0. by rewrite addSnnS -{1}[val i]addn0 /= => /addnI. rewrite big_ord_recr /= big1 ?mul1r; last first. case=> j /= lt_ji _; rewrite FE; last first. by rewrite (@leq_trans i) // ltnW. by rewrite eq_sym (ltn_eqF lt_ji) expr0. by rewrite FE // eqxx expr1 /inj /insubd valK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg