proposition: Lemma put_backK n (i : 'I_n.+1) : cancel (put_front i) (put_back i).
proof: Proof. move=> j; rewrite /put_back /put_front; case: (ifPn (j == i)) => [ji|]. rewrite eqxx; exact/esym/eqP. rewrite neq_ltn => /orP[|] ji. rewrite ji ifF; last first. apply/negbTE/eqP => /(congr1 val) => /=. by rewrite inordK // ltnS (leq_trans ji) // -ltnS. rewrite inordK; last by rewrite ltnS (leq_trans ji) // -ltnS. by rewrite ji /=; apply val_inj => /=; rewrite inordK. rewrite ltnNge (ltnW ji) /= ifF; last first. by apply/negbTE; rewrite -lt0n (leq_trans _ ji). by rewrite leqNgt ji. 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