∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [Module.Finite R E], Module.Finite { c // 0 ≤ c } E