have h2: NeZero (p*q) := by
  apply ne_zero_product_of_primes hp hq
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1
p q : ℕ
hp : Nat.Prime p
hq : Nat.Prime q
list1 : Fintype (ZMod (p * q))ˣ
h2 : NeZero (p * q)
⊢ ∀ (t : (ZMod (p * q))ˣ), t ^ φ (p * q) = 1