fact: Fixpoint Convn (A : convType) n : {fdist 'I_n} -> ('I_n -> A) -> A := match n return forall (e : {fdist 'I_n}) (g : 'I_n -> A), A with | O => fun e g => False_rect A (fdistI0_False e) | m.+1 => fun e g => match Bool.bool_dec (e ord0 == 1%coqR) true with | left _ => g ord0 | right H => let G := fun i => g (fdist_del_idx ord0 i) in g ord0 <| probfdist e ord0 |> Convn (fdist_del (Bool.eq_true_not_negb _ H)) G end end.
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