proposition: Lemma I3P i : I3_spec i (i == inord 0) (i == inord 1) (i == inord 2).
proof: Proof. have : i \in map inord (iota 0 3). apply/mapP. exists (nat_of_ord i). by rewrite mem_iota leq0n add0n ltn_ord. by rewrite inord_val. rewrite inE => /orP[/eqP ->|]. rewrite eqxx. do 2 I3_neq. exact: I2_0. rewrite inE => /orP[/eqP ->|]. rewrite eqxx. I3_neq. I3_neq. exact: I2_1. rewrite inE => /eqP ->. rewrite eqxx. I3_neq. I3_neq. exact: I2_2. Qed.
imports: mathcomp(all_ssreflect ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext fdist proba