proposition: Lemma card_supp_fdistD1 (Xb0 : X b != 0) : #|fdist_supp (fdistD1 Xb1)| = #|fdist_supp X|.-1.
proof: Proof. rewrite /fdist_supp (cardsD1 b [set a | X a != 0]) !inE Xb0 add1n /=. apply eq_card => i; rewrite !inE fdistD1E. case: ifPn => //= ib; first by rewrite eqxx. apply/idP/idP; first by apply: contra => /eqP ->; rewrite mul0r. apply: contra. rewrite mulf_eq0 => /orP[// | H]. exfalso. move/negPn/negP : H; apply. by rewrite invr_neq0// subr_eq0 eq_sym. 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