proposition: Lemma isd_mflip xt : isdistr (mflip xt).
proof: Proof. apply/isdistr_finP; split=> [b|]. + by case: b; rewrite ?subr_ge0 cp01_clamp. + by rewrite /index_enum !unlock /= addr0 addrCA subrr addr0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum