fact: CoInductive I3_spec : 'I_3 -> bool -> bool -> bool -> Prop := | I2_0 : I3_spec (inord 0) true false false | I2_1 : I3_spec (inord 1) false true false | I2_2 : I3_spec (inord 2) false false true.
imports: mathcomp(all_ssreflect ssrnum) Reals Lra mathcomp(Rstruct) ssrR Reals_ext fdist proba