proposition: Lemma fdist_col'_put_front n (A : finType) (P : {fdist 'rV[A]_n.+1}) (i : 'I_n.+1) : i != ord0 -> fdist_col' P i = (fdist_prod_of_rV (fdist_perm P (put_front_perm i)))`2.
proof: Proof. move=> i0; apply/fdist_ext => /= v; rewrite fdist_col'E fdist_sndE. destruct n as [|n']; first by rewrite (ord1 i) eqxx in i0. transitivity (\sum_(x : A) P (\row_(k < n'.+2) (if k == i then x else v ``_ (inord (unbump i k)))))%R. rewrite (reindex_onto (fun a => \row_k (if k == i then a else v ``_ (inord (unbump i k)))) (fun w => w ``_ i)); last first. move=> w wv. apply/rowP => j. rewrite !mxE; case: ifPn => [/eqP -> //|ji]. rewrite -(eqP wv) mxE; congr (w _ _). move: ji; rewrite neq_ltn => /orP[|] ji. apply val_inj => /=. rewrite inordK; last first. by rewrite /unbump (ltnNge i j) (ltnW ji) subn0 (leq_trans ji) // -ltnS. by rewrite unbumpK //= inE ltn_eqF. apply val_inj => /=. rewrite inordK; last first. by rewrite /unbump ji subn1 prednK //; [rewrite -ltnS | rewrite (leq_ltn_trans _ ji)]. by rewrite unbumpK //= inE gtn_eqF. apply eq_bigl => a /=. apply/andP; split. apply/eqP/rowP => k. rewrite !mxE eq_sym (negbTE (neq_lift _ _)). congr (v _ _). apply val_inj => /=. by rewrite bumpK inordK. by rewrite mxE eqxx. under [RHS] eq_bigr do rewrite fdist_prod_of_rVE fdist_permE. apply/eq_bigr => a _; congr (P _); apply/rowP => k /=. rewrite /col_perm /= 2!mxE /=. rewrite /put_front_perm /= permE /put_front. case: ifPn => [ki|]; first by rewrite row_mx_row_ord0. rewrite neq_ltn => /orP[|] ki. rewrite ki. rewrite (_ : inord _ = rshift 1 (inord k)); last first. apply/val_inj => /=. rewrite add1n inordK /=. by rewrite inordK // (leq_trans ki) // -ltnS. by rewrite ltnS (leq_trans ki) // -ltnS. rewrite (@row_mxEr _ _ 1); congr (v ``_ _). apply val_inj => /=. rewrite /unbump ltnNge (ltnW ki) subn0 inordK //. by rewrite (leq_trans ki) // -ltnS. rewrite ltnNge (ltnW ki) /=; move: ki. have [/eqP -> //|k0] := boolP (k == ord0). rewrite (_ : k = rshift 1 (inord k.-1)); last first. by apply val_inj => /=; rewrite add1n inordK ?prednK // ?lt0n // -ltnS. rewrite (@row_mxEr _ 1 1) /=. rewrite inordK ?prednK ?lt0n // -1?ltnS // ltnS add1n prednK ?lt0n // => ik. by congr (v _ _); apply val_inj => /=; rewrite /unbump ik subn1. Qed.
imports: mathcomp(all_ssreflect all_algebra fingroup perm matrix) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext bigop_ext logb ln_facts fdist jfdist_cond proba binary_entropy_function divergence