proposition: Lemma ConvnI1E (g : 'I_1 -> T) (e : {fdist 'I_1}) : <|>_ e g = g ord0.
proof: Proof. rewrite /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H. exfalso; move/eqP: H; apply. by apply/eqP; rewrite fdist1E1 (fdist1I1 e). 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