proposition: Lemma fdist1I1 (d : R.-fdist 'I_1) : d = fdist1 ord0 :> fdist R _.
proof: Proof. apply/fdist_ext => /= i; rewrite fdist1E (ord1 i) eqxx. by move: (FDist.f1 d); rewrite big_ord_recl big_ord0 addr0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext