proposition: Lemma fdist_ind (P : fdist R A -> Type) : (forall n : nat, (forall X, #|fdist_supp X| = n -> P X) -> forall X b, #|fdist_supp X| = n.+1 -> X b != 0 -> P X) -> forall X, P X.
proof: Proof. move=> H1 d. move: {-2}(#|fdist_supp d|) (erefl (#|fdist_supp d|)) => n; move: n d. elim=> [d /esym /card0_eq Hd0|n IH d n13]. move: (FDist.f1 d). rewrite -[X in X = _]mulr1 big_distrl sum_fdist_supp big1 => [|a]. by move=> /esym/eqP; rewrite oner_eq0. by rewrite Hd0. have [b Hb] : {b : A | d b != 0}. suff : {x | x \in fdist_supp d} by case => a; rewrite inE => ?; exists a. by apply/sigW/set0Pn; rewrite -cards_eq0 -n13. by refine (H1 n _ _ _ _ Hb) => // d' A2; apply IH. 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