proposition: Lemma Convn_perm_tperm (n : nat) (d : {fdist 'I_n.+3}) (g : 'I_n.+3 -> A) (s : 'S_n.+3) (H : s = tperm ord0 (lift ord0 ord0)) (dmax1 : d ord0 != 1%coqR) (m : nat) (nm : (n.+3 < m.+1)%nat) (IH : forall n : nat, (n < m)%nat -> forall (d : {fdist 'I_n}) (g : 'I_n -> A) (s : 'S_n), <|>_d g = <|>_(fdistI_perm d s) (g \o s)) : <|>_d g = <|>_(fdistI_perm d s) (g \o s).
proof: Proof. have [K|K] := eqVneq (d (lift ord0 ord0)) (1 - d ord0). case/boolP : (d (lift ord0 ord0) == 1%coqR :> R) => [|d11]. by rewrite fdist1E1 => /eqP ->; rewrite fdistI_perm_fdist1 !Convn_fdist1 /= permKV. rewrite convnE. rewrite [in RHS]convnE. by rewrite fdistI_permE H permE. move=> K'. rewrite (_ : <|>_ _ _ = g (lift ord0 ord0)); last first. have /eqP : (fdist_del dmax1) ord0 = 1%coqR. by rewrite fdist_delE fdistD1E /= K divrr // unitfE subr_eq0 eq_sym. rewrite fdist1E1 => /eqP ->. by rewrite Convn_fdist1. rewrite (_ : <|>_ _ _ = g ord0); last first. have /eqP : (fdist_del K') ord0 = 1%coqR. rewrite fdist_delE fdistD1E /= !fdistI_permE H !permE /=. rewrite K opprB (addrC (d _) (-1)) addrA subrr add0r divrr // unitfE. apply /eqP => d00. by move: K; rewrite d00 subr0; apply/eqP. by rewrite fdist1E1 => /eqP ->; rewrite Convn_fdist1 /= H !permE /=. rewrite convC /= H permE /=; congr (_ <| _ |> _). by apply val_inj => /=; rewrite fdistI_permE /= permE /= K. have [/eqP |K1] := eqVneq (d (lift ord0 ord0)) 1%coqR. by rewrite fdist1E1 => /eqP ->; rewrite fdistI_perm_fdist1 !Convn_fdist1 /= permKV. pose D' : {ffun 'I_3 -> R} := [ffun x => [eta (fun=>R0) with ord0 |-> d ord0, lift ord0 ord0 |-> d (lift ord0 ord0), ord_max |-> (\sum_(i < n.+3 | (2 <= i)%nat) d i)%coqR] x]. have D'0 : (forall i, 0 <= D' i). move=> i; rewrite /D' ffunE /=; case: ifPn => _ //. by case: ifPn => _ //; case: ifPn => _; [exact: sumr_ge0 | exact/lexx]. have D'1 : (\sum_(i < 3) (D' i) = 1). rewrite !big_ord_recr big_ord0 /= add0r. rewrite /D' !ffunE /= -(FDist.f1 d). apply/esym. rewrite 2!big_ord_recl addrA; congr (_ + _)%coqR. apply/esym. set h : 'I_n.+1 -> 'I_n.+3 := fun i => lift ord0 (lift ord0 i). set h' : 'I_n.+3 -> 'I_n.+1 := fun i => inord (i.-2). rewrite (reindex_onto h h'); last first. move=> j /= j1. rewrite /h /h'. apply val_inj => /=. rewrite /bump /bump !leq0n !add1n inordK //; last first. rewrite prednK; last by rewrite -subn1 subn_gt0. by rewrite -subn1 leq_subLR add1n -ltnS. rewrite prednK; last by rewrite -subn1 subn_gt0. by rewrite prednK // (leq_trans _ j1). apply eq_big => //= i. rewrite /h' /h. by apply/eqP/val_inj => /=; rewrite inordK. set D := FDist.make D'0 D'1. have H1 : (fdist_del dmax1) ord0 != 1%coqR. rewrite fdist_delE fdistD1E (eq_sym (lift _ _)) (negbTE (neq_lift _ _)). apply/eqP. move/divr1_eq. exact/eqP. pose G : 'I_3 -> A := [eta (fun=>g ord0) with ord0 |-> g ord0, lift ord0 ord0 |-> g (lift ord0 ord0), ord_max |-> <|>_(fdist_del H1) (fun i : 'I_n.+1 => g (lift ord0 (lift ord0 i)))]. transitivity (Convn D G). erewrite convn3E. rewrite convnE. congr (_ <| _ |> _). by apply/val_inj => /=; rewrite ffunE. rewrite convnE. rewrite /G. congr (_ <| _ |> _). by rewrite ffunE. by rewrite /= !ffunE fdist_delE fdistD1E. rewrite (Convn_permI3 _ _ S3.p01). pose q' := (d ord0 / (1 - d (lift ord0 ord0))). move=> [:Hq]. have @q : {prob R}. apply: (@Prob.mk_ _ q'). abstract: Hq. apply/andP. split. by apply/divr_ge0/ltW => //; rewrite subr_gt0 -fdist_lt1. rewrite ler_pdivrMr. rewrite mul1r. rewrite lerBrDr -(FDist.f1 d). rewrite 2!big_ord_recl addrA lerDl. by apply: sumr_ge0 => i _. by rewrite subr_gt0 -fdist_lt1. rewrite (@convn3E _ _ q); last 2 first. rewrite fdistI_permE permE /= (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. by rewrite /D' ffunE /=. rewrite /= !fdistI_permE /= !permE /= (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. by rewrite !ffunE. rewrite convnE. by rewrite fdistI_permE H !permE. move=> K2. congr (_ <| _ |> _). apply val_inj => /=. rewrite !fdistI_permE !permE /= (_ : Ordinal _ = lift ord0 ord0); last exact/val_inj. by rewrite ffunE H !permE. by rewrite /= /G /= permE /= H permE /=. rewrite convnE. rewrite fdist_delE fdistD1E !fdistI_permE H !permE /=. apply/eqP. move/divr1_eq. by move/eqP; rewrite eq_sym subr_eq addrC -subr_eq; apply/negP; rewrite eq_sym. move=> K3. congr (_ <| _ |> _). apply val_inj => /=. by rewrite !fdist_delE !fdistD1E /= !fdistI_permE H !permE. by rewrite /= /G /= !permE /= /fdist_del_idx ltnn H permE /=. pose s' : 'S_n.+1 := 1%g. rewrite (@IH _ _ _ _ s') //; last by rewrite -ltnS ltnW. transitivity (<|>_(fdist_del H1) (fun i : 'I_n.+1 => g (lift ord0 (lift ord0 i)))). by rewrite /G [in LHS]/= !permE [in LHS]/=. congr (Convn _ _). apply/fdist_ext => j. rewrite !(fdist_delE,fdistI_permE,fdistD1E). rewrite H !permE /=. rewrite -!mulrA. congr (_ * _). have d0_1 : 1 - d ord0 != 0; first by rewrite subr_eq0 eq_sym. rewrite -[I in I - _ / _](mulfV d0_1). rewrite -mulrBl invf_div mulrA mulVf //. have dl0_1 : 1 - d (lift ord0 ord0) != 0; first by rewrite subr_eq0 eq_sym. rewrite -[I in I - _ / _](mulfV dl0_1) -mulrBl invf_div mulrA mulVf //. by rewrite addrAC. by rewrite boolp.funeqE => j; rewrite /= permE H permE. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix fingroup perm) Reals Lra mathcomp(mathcomp_extra Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext logb fdist convex