proposition: Lemma eq_dec_refl i : Nat.eq_dec i i = left (erefl i).
proof: Proof. case: Nat.eq_dec => Hi; last by elim Hi. congr left; by rewrite (Eqdep_dec.UIP_refl_nat _ Hi). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) mathcomp(Rstruct) Reals ssrR Reals_ext logb ssr_ext ssralg_ext bigop_ext fdist proba