∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V]
  (motive : ℕ → ConvexBody V → Prop) (x : ℕ) (x_1 : ConvexBody V),
  (∀ (x : ConvexBody V), motive 0 x) → (∀ (n : ℕ) (K : ConvexBody V), motive n.succ K) → motive x x_1