proposition: Lemma e0_delta : e0 <> delta.
proof: Proof. rewrite /e0 /delta /lambda -/r. apply Rmin_case_strong => H1; first by lra. apply Rmin_case_strong => H2. - apply/eqP/gtR_eqF; apply: leR_ltR_trans. + apply: (leR_trans _ H2). rewrite leR_pdivr_mulr //; apply leR_pmulr; [lra|exact/ltRW/Hepsilon1]. * rewrite ltR_pdivr_mulr //; lra. - by rewrite /Rdiv -mulRA (_ : ( _ * / 2 ) = / 4); [lra | field]. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) Reals Lra mathcomp(Rstruct) ssrR Reals_ext realType_ext logb fdist proba entropy aep typ_seq source_code