proposition: Lemma convn3E (g : 'I_3 -> A) (d : {fdist 'I_3}) (p : {prob R}) : d ord0 != 1%R -> (d (lift ord0 ord0) / (1 - d ord0)) = Prob.p p -> <|>_d g = g ord0 <| probfdist d ord0 |> (g (Ordinal (erefl (1 < 3)%nat)) <| p |> g (Ordinal (erefl (2 < 3)%nat))).
proof: Proof. move=> i1 Hp. have [p1|p1] := eqVneq p 1%:pr. rewrite convnE; congr (_ <| _ |> _). rewrite convn2E /fdist_del_idx ltnn /=; congr (g _ <| _ |> g _). apply val_inj => /=. by rewrite fdist_delE fdistD1E (eq_sym (lift _ _)) (negbTE (neq_lift _ _)). exact/val_inj. exact/val_inj. rewrite convnE; congr (_ <| _ |> _). rewrite convn2E /fdist_del_idx ltnn /=; congr (g _ <| _ |> g _). - apply val_inj => /=. by rewrite fdist_delE fdistD1E (eq_sym (lift _ _)) (negbTE (neq_lift _ _)). - exact/val_inj. - exact/val_inj. 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