theorem ex2.{u_1} : ∀ {α : Type u_1} [inst : S α],
  100000000000000000 * 20000000000000000 = 2000000000000000000000000000000000 :=
fun {α} [S α] => S.ofNat_mul 100000000000000000 20000000000000000