proposition: Lemma ball_le x : {homo ball x : e1 e2 / e1 <= e2 >-> e1 `<=` e2}.
proof: Proof. move=> e1 e2 le12 y xe1_y. move: le12; rewrite le_eqVlt => /orP [/eqP <- //|]. rewrite -subr_gt0 => lt12. rewrite -[e2](subrK e1); apply: ball_triangle xe1_y. suff : ball x (PosNum lt12)%:num x by []. exact: ball_center. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed