proposition: Lemma convn_proj n (g : 'I_n -> A) (d : {fdist 'I_n}) i : d i = R1 -> <|>_d g = g i.
proof: Proof. elim: n g d i => [d d0|n IH g d i di1]; first by move: (fdistI0_False d0). have [i0|i0] := eqVneq i ord0. move/eqP : di1; rewrite i0 fdist1E1 => /eqP ->. by rewrite Convn_fdist1. have d00 : d ord0 = R0 by move/eqP/fdist1P : di1 => -> //; rewrite eq_sym. rewrite convnE; first by rewrite d00; apply/eqP; lra. move=> d01. rewrite (_ : probfdist _ _ = 0%:pr); last exact/val_inj. rewrite conv0. move=> [:Hj]. have @j : 'I_n. apply: (@Ordinal _ i.-1). abstract: Hj; by rewrite prednK // ?lt0n // -ltnS. rewrite (IH _ _ j) // ?ltn0. congr g; apply val_inj => /=. by rewrite /bump leq0n add1n prednK // lt0n. rewrite fdist_delE ltn0 fdistD1E eq_sym (negbTE (neq_lift _ _ )). rewrite d00 subr0 divr1 -di1; congr (d _). 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