proposition: Lemma ConvnI2E (g : 'I_2 -> T) (d : {fdist 'I_2}) : <|>_d g = g ord0 <| probfdist d ord0 |> g (lift ord0 ord0).
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 ConvnIE; congr (_ <| _ |> _). by rewrite ConvnI1E /fdist_del_idx ltnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist