proposition: Theorem rsa_correct r w : decrypt r (encrypt r w) = w %[mod p r * q r].
proof: Proof. case/and5P: (wf r) => Pp Pq pDq pq_gt0 /and3P[pDpq qDpq /eqP edE]. have pCq : coprime (p r) (q r) by rewrite prime_coprime ?dvdn_prime2. have pq_gt1 : 1 < pq r. by case: p q Pp Pq pDq pq_gt0 pDpq qDpq => [] [|[|p1]] // [|[|[|q1]]] //; case: pq => [|[|]]. have ed_gt0 : 0 < e r * d r. by case: (_ * _) edE; rewrite // mod0n [1 %% _]modn_small. rewrite /decrypt /encrypt modnXm modn_mod -expnM. apply/eqP; rewrite chinese_remainder //. apply/andP; split. have [pDw|/negP pNDw] := boolP (p r %| w). by rewrite -modnXm (eqP pDw) exp0n ?mod0n. rewrite (divn_eq (_ * _) (pq r)) edE [1 %% _]modn_small // addn1 expnS. rewrite -[X in _ == X %% _]muln1 -modnMmr -[_ * 1 %% _]modnMmr. apply/eqP; congr (_ * _ %% _). rewrite mulnC expnM -(exp1n ((e r * d r) %/ pq r)). rewrite -[LHS]modnXm -[RHS]modnXm; congr (_ ^ _ %% _). have /dvdnP[k ->] := pDpq. rewrite mulnC expnM -[LHS]modnXm fermat_little_pred //. by rewrite modnXm exp1n. have [qDw|/negP qNDw] := boolP (q r %| w). by rewrite -modnXm (eqP qDw) exp0n ?mod0n. rewrite (divn_eq (_ * _) (pq r)) edE [1 %% _]modn_small // addn1 expnS. rewrite -[X in _ == X %% _]muln1 -modnMmr -[_ * 1 %% _]modnMmr. apply/eqP; congr (_ * _ %% _). rewrite mulnC expnM -(exp1n ((e r * d r) %/ pq r)). rewrite -[LHS]modnXm -[RHS]modnXm; congr (_ ^ _ %% _). have /dvdnP[k ->] := qDpq. rewrite mulnC expnM -[LHS]modnXm fermat_little_pred //. by rewrite modnXm exp1n. Qed.
imports: mathcomp(all_ssreflect)