proposition: Lemma axbarypart : ax_bary_part T.
proof: Proof. move=> n m d e g HP. have [n0 Hn0] := fdist_supp_mem d. set h' : 'I_n -> 'I_#|fdist_supp d| := enum_rank_in Hn0. set h : 'I_#|fdist_supp d| -> 'I_n := enum_val. have f j : {i | [forall i, j \notin fdist_supp (e (h i))]||(j \in fdist_supp (e (h i)))}. case/boolP: [forall i, j \notin fdist_supp (e (h i))]. by move=> _; exists (proj1_sig (fdist_supp_mem (fdistmap h' d))). by rewrite -negb_exists negbK => /existb_sig. rewrite /= in f. rewrite [LHS](axpart h'). rewrite [RHS](axpart (fun j => proj1_sig (f j))). have trivIK i j x : x \in fdist_supp (e i) -> x \in fdist_supp (e j) -> i = j. have [|] := eqVneq i j => [// | ij] xi xj. move/setP/(_ x): (HP _ _ ij); by rewrite inE xi xj inE. have neqj j a k : a \in fdist_supp (e (h j)) -> k != (h j) -> (d k * e k a = 0)%R. move=> Haj kj. case/boolP: (a \in fdist_supp (e k)) => [ak|]. by rewrite (trivIK _ _ _ Haj ak) eqxx in kj. rewrite inE negbK => /eqP ->. by rewrite mulR0. have Hmap' i : fdistmap h' d i = (\sum_j d (h i) * e (h i) j)%R. rewrite -big_distrr fdistE /= FDist.f1 /= mulR1. rewrite (bigD1 (h i)) /=; last by rewrite /h /h' !inE enum_valK_in eqxx. rewrite big1 /= ?addr0 // => j /andP[] /eqP <-. case /boolP: (j \in fdist_supp d) => Hj. by rewrite /h /h' (enum_rankK_in Hn0 Hj) eqxx. move: Hj; by rewrite inE negbK => /eqP. have Hmap i : fdistmap (fun j : 'I_m => sval (f j)) (fdist_convn d e) i = fdistmap h' d i. rewrite fdistE big_mkcond /=. under eq_bigr do rewrite fdistE. rewrite (eq_bigr (fun j => d (h i) * e (h i) j)%R). by rewrite Hmap'. move=> /= a _; rewrite !inE; case: (f a) => j /= /orP[/forallP /= |] Ha. have Ha0 k : (d k * e k a = 0)%R. case/boolP: (k \in fdist_supp d) => [Hk|]. move: (Ha (h' k)). by rewrite inE negbK /h/h' enum_rankK_in // => /eqP ->; rewrite mulR0. by rewrite inE negbK => /eqP -> ; rewrite mul0R. case: ifPn => [/eqP|] _. by rewrite Ha0 big1. by rewrite Ha0. case: ifPn => [/eqP/esym ->{i}|ji]. by rewrite (bigD1 (h j)) //= big1 ?addr0 // => *; rewrite -RmultE (neqj j). by rewrite (neqj j) //; apply: contra ji => /eqP/enum_val_inj ->. congr (<&>_ _ _); first by apply fdist_ext => /= i; rewrite Hmap. apply funext => i /=. have HF : fdistmap h' d i != 0%R. rewrite fdistE /=. apply/eqP => /psumr_eq0P H. have: h i \in fdist_supp d by apply enum_valP. by rewrite inE H ?eqxx // 2!inE /h /h' enum_valK_in. rewrite (@axidem (<&>_(e (h i)) g)); last first. move=> /= j; rewrite inE. rewrite FDistPart.dE //. case/boolP: (j \in fdist_supp d) => [Hj|]. case: (@eqP _ i) => [-> |]. by rewrite /h /h' (enum_rankK_in _ Hj). by rewrite /Rdiv mulR0 mul0R eqxx. by rewrite inE negbK => /eqP ->; rewrite mul0R div0R eqxx. congr (<&>_ _ _); apply fdist_ext => j. rewrite FDistPart.dE; last first. rewrite !fdistE /=. under eq_bigr do rewrite fdistE. rewrite exchange_big /=. rewrite (bigD1 (h i)) //=. rewrite -big_distrr big_mkcond /=. rewrite (eq_bigr (e (h i))). rewrite FDist.f1 mulr1; apply paddR_neq0 => //. by apply/RleP/sumr_ge0 => *; apply/sumr_ge0 => *; rewrite mulr_ge0. by left; move: (enum_valP i); rewrite inE. move=> /= k _; rewrite 2!inE; case: ifP => //. case: (f k) => /= x /orP[/forallP/(_ i)|Hkx Hx]. by rewrite inE negbK => /eqP ->. case/boolP: (k \in fdist_supp (e (h i))) => [Hki |]. move/eqP: (trivIK _ _ _ Hkx Hki) Hx. by rewrite (can_eq (enum_valK_in Hn0)) => ->. by rewrite inE negbK => /eqP ->. move: (Hmap i). rewrite fdistE /= => ->. rewrite fdistE. case: (f j) => /= k /orP[Hn|jk]. move/forallP/(_ i): (Hn). rewrite inE negbK => /eqP ->. rewrite big1 /Rdiv ?mul0R //. move=> a _. move/forallP/(_ (h' a)): Hn. case/boolP: (a \in fdist_supp d). rewrite /h /h'. move/(enum_rankK_in _) ->. by rewrite inE negbK => /eqP ->; rewrite mulr0. by rewrite inE negbK => /eqP ->; rewrite mul0r. rewrite (bigD1 (h k)) //= big1 ?addR0; last first. by move=> a Ha; apply (neqj k). case/boolP: (j \in fdist_supp (e (h i))) => ji. have /enum_val_inj H := trivIK _ _ _ jk ji. subst k => {jk}. move: HF; rewrite eqxx mulR1 Hmap'. rewrite -big_distrr /= FDist.f1 mulR1 => HF. rewrite addr0 -RmultE. by rewrite /Rdiv mulRAC mulRV // mul1R. case: eqP ji => [->|ik]; first by rewrite jk. by rewrite inE negbK => /eqP ->; rewrite mulR0 div0R. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex