rw [mul_one, Nat.mod_mod]
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
k : ℕ
hk : public_key * private_key = 1 + (p - 1) * (q - 1) * k
⊢ message % (p * q) * 1 % (p * q) = message % (p * q)
no goals