proposition: Lemma fdist_convn_del (R : realType) (A : finType) (n : nat) (g : 'I_n.+1 -> {fdist A}) (P : {fdist 'I_n.+1}) (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) : let g' := fun i : 'I_n => g (fdist_del_idx j i) in fdist_convn P g = (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist.
proof: Proof. move=> g' /=; apply/fdist_ext => a. rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _). rewrite fdist_convnE big_distrr /=. rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=. rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _). rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW. move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS. move=> jn'. apply/eq_big. by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. move=> /= i _. rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first. by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. rewrite mulrA mulrCA mulrV ?mulr1; last first. rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //. congr (P _ * _); first exact/val_inj. by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj. rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first. move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle. rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first. move=> i; by rewrite -leqNgt. rewrite big_mkcond. rewrite big_ord_recl ltn0 /= add0r. rewrite [in RHS]big_mkcond. apply eq_bigr => i _. rewrite /bump add1n ltnS; case: ifPn => // ji. rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first. apply/eqP => /(congr1 val) => /=. rewrite /bump add1n => ij. by move: ji; apply/negP; rewrite -ij ltnn. rewrite -mulrAC [in RHS]mulrC 3!mulrA divrr ?mul1r ?unitfE ?onem_neq0 //. by rewrite /g' /fdist_del_idx ltnNge ji. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist