proposition: Lemma Convn_perm_projection n (d : {fdist 'I_n.+2}) (g : 'I_n.+2 -> A) (s : 'S_n.+2) (H : s ord0 = ord0) (dmax1 : d ord0 != 1%coqR) (m : nat) (nm : (n.+1 < m)%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. transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdist_del dmax1) (fun x => g (fdist_del_idx ord0 x)))). by rewrite convnE. set s' : 'S_n.+1 := PermDef.perm (Sn.proj0_inj H). transitivity (g ord0 <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))). by rewrite -IH. transitivity (g (s ord0) <| probfdist d ord0 |> (<|>_(fdistI_perm (fdist_del dmax1) s') ((fun x => g (fdist_del_idx ord0 x)) \o s'))). by rewrite H. rewrite [in RHS]convnE //. by rewrite fdistI_permE H. move=> K. congr (_ <| _ |> _). apply val_inj => /=; by rewrite fdistI_permE H. congr (Convn _ _). apply/fdist_ext => /= j. rewrite !fdistI_permE !fdist_delE !fdistD1E !fdistI_permE. rewrite /s' /=. rewrite permE. rewrite /f /=. rewrite H; congr (_ / _). congr (d _). apply val_inj => /=. rewrite /bump leq0n add1n /=. rewrite inordK //; last first. rewrite prednK //. by rewrite -ltnS. rewrite lt0n. suff : s (lift ord0 j) != ord0 by []. rewrite -[in X in _ != X]H. by apply/eqP => /(@perm_inj _ s). rewrite prednK // lt0n. suff : s (lift ord0 j) != ord0 by []. rewrite -[in X in _ != X]H. by apply/eqP => /(@perm_inj _ s). rewrite boolp.funeqE => j /=. rewrite /fdist_del_idx /= /s' permE /f /=. congr g. apply val_inj => /=. rewrite /bump leq0n add1n /=. rewrite inordK //; last first. rewrite prednK //. by rewrite -ltnS. rewrite lt0n. suff : s (lift ord0 j) != ord0 by []. rewrite -[X in _ != X]H. by apply/eqP => /(@perm_inj _ s). rewrite prednK // lt0n. suff : s (lift ord0 j) != ord0 by []. rewrite -[X in _ != X]H. by apply/eqP => /(@perm_inj _ s). 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