proposition: Lemma convn2E (g : 'I_2 -> A) (d : {fdist 'I_2}) : <|>_d g = g ord0 <| probfdist d ord0 |> g (Ordinal (erefl (1 < 2))).
proof: Proof. have [/eqP |i1] := eqVneq (d ord0) 1%coqR. rewrite fdist1E1 => /eqP ->; rewrite Convn_fdist1. rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //. by apply val_inj; rewrite /= fdist1xx. rewrite convnE; congr (_ <| _ |> _). rewrite (_ : (fun _ => _) = (fun=> g (fdist_del_idx ord0 ord0))); last first. by rewrite boolp.funeqE => x; rewrite (ord1 x). by rewrite convn1E /fdist_del_idx ltnn; congr g; 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