have h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1)*(q - 1)*k := 
  sorry
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message
msg : ℕ
p q public_key private_key message : ℕ
hp : Prime p
hq : Prime q
h_pub_pri : public_key * private_key ≡ 1 [MOD (p - 1) * (q - 1)]
h_msg : message < p * q
h_rel_prime : Nat.gcd msg (p * q) = 1
h_lin_combo : ∃ k, public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message