proposition: Lemma jtype_0_jtypef (V : P_ n ( A , B )) a b : V a b = 0%R -> (JType.f V) a b = ord0.
proof: Proof. destruct V as [V1 V2 V3 V4] => /=. rewrite V4 /=. case: ifP => [| H']. rewrite sum_nat_eq0. move/forallP/(_ b)/implyP/(_ Logic.eq_refl)/eqP => H _; exact: val_inj. rewrite /Rdiv mulR_eq0 => -[|abs]. rewrite INR_eq0 => ?; exact/val_inj. exfalso. by apply/eqP : abs; apply/invR_neq0'; rewrite INR_eq0' H'. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum fingroup perm) Reals mathcomp(Rstruct) ssrR Reals_ext realType_ext ssr_ext ssralg_ext logb fdist entropy num_occ channel types