∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.MonObj N] (n : ℕ) (x : CategoryTheory.Conv M N),
  npowRecAuto (n + 1) x = npowRecAuto n x * x