proposition: Lemma fdistD1_eq0 a (Xa0 : X a != 0) : ((fdistD1 Xb1 a == 0) = (b == a))%bool.
proof: Proof. rewrite fdistD1E; case: ifPn => [/eqP ->|ab]; first by rewrite !eqxx. apply/idP/idP => [|]; last by rewrite eq_sym (negbTE ab). rewrite mulf_eq0 => /orP[]; first by rewrite (negbTE Xa0). by rewrite invr_eq0 subr_eq0 eq_sym (negbTE Xb1). 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