∀ (α : Type u) {β : Type v} [inst : AddGroup α] [inst_1 : AddAction α β] (b : β) [inst_2 : Fintype α]
  [inst_3 : Fintype ↑(AddAction.orbit α b)] [inst_4 : Fintype ↥(AddAction.stabilizer α b)],
  Fintype.card ↑(AddAction.orbit α b) * Fintype.card ↥(AddAction.stabilizer α b) = Fintype.card α