proposition: Lemma ConvnI1_eq n (g : 'I_n -> T) (d : {fdist 'I_n}) (n1 : n = 1) (i : 'I_n) : <|>_d g = g i.
proof: Proof. rewrite ConvnI1_eq_rect. have -> /= : eq_rect n (fun n0 : nat => 'I_n0 -> T) g 1 n1 = g \o eq_rect 1 (fun n0 : nat => 'I_1 -> 'I_n0) idfun n (esym n1) by subst n. have /(_ i) I_n_contr : forall a b : 'I_n, a = b by rewrite n1 => a b; rewrite (ord1 a) (ord1 b). by rewrite -(I_n_contr (eq_rect 1 (fun n => 'I_1 -> 'I_n) idfun n (esym n1) ord0)). 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