proposition: Lemma binconv1 a b : binconv 1%:pr a b = a.
proof: Proof. apply axidem => /= i; rewrite inE fdistI2E; case: ifP => //=. by rewrite /onem subrr eqxx. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex