proposition: Lemma Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> A): <|>_(fdist1 j) g = g j.
proof: Proof. elim: n j g => [[] [] //|n IH j g /=]. case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01]. rewrite fdist1E; case j0 : (_ == _) => /=. by move=> _; rewrite (eqP j0). by move/eqP; rewrite eq_sym R1E oner_eq0. rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last first. apply val_inj => /=; move: b01; rewrite !fdist1E => j0. by case j0' : (_ == _) => //; rewrite j0' eqxx in j0. have j0 : ord0 != j by apply: contra b01 => /eqP <-; rewrite fdist1xx. have j0' : 0 < j by rewrite lt0n; apply: contra j0 => /eqP j0; apply/eqP/val_inj. move=> [:H]; have @j' : 'I_n. by apply: (@Ordinal _ j.-1 _); abstract: H; rewrite prednK // -ltnS. rewrite (_ : fdist_del b01 = fdist1 j'); last first. apply/fdist_ext => /= k. rewrite fdist_delE fdistD1E /= !fdist1E /= (negbTE j0) subr0 divr1. congr (GRing.natmul _ (nat_of_bool _)). move R : (k == _) => [|]. - apply/eqP/val_inj; rewrite /= /bump leq0n add1n. by move/eqP : R => -> /=; rewrite prednK // lt0n. - apply: contraFF R => /eqP. move/(congr1 val) => /=; rewrite /bump leq0n add1n => kj. by apply/eqP/val_inj; rewrite /= -kj. rewrite IH /fdist_del_idx ltn0; congr g. by apply val_inj; rewrite /= /bump leq0n add1n prednK // lt0n. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex