no goals
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NormedSpace ℝ V
K✝ L✝ K L : ConvexBody V
⊢ EMetric.hausdorffEdist ↑K ↑L ≠ ⊤
apply_rules [Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded, ConvexBody.nonempty,
  ConvexBody.bounded]