dsimp [rsa_decrypt, rsa_encrypt]
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
⊢ rsa_decrypt private_key (p * q) (rsa_encrypt public_key (p * q) message) = 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
⊢ (message ^ public_key % (p * q)) ^ private_key % (p * q) = message