如何优化Coq中部分学外延性定理的证明脚本

我从事部分学研究，想要证明外延性（Extensionality）定理可由我设定的四条公理推导得出。

基础定义与公理代码 #

Require Import Classical.
Parameter Entity: Set.
Parameter P : Entity -> Entity -> Prop.

Axiom P_refl : forall x, P x x.

Axiom P_trans : forall x y z,
  P x y -> P y z -> P x z.

Axiom P_antisym : forall x y,
  P x y -> P y x -> x = y.

Definition PP x y := P x y /\ x <> y.
Definition O x y := exists z, P z x /\ P z y.

Axiom strong_supp : forall x y,
  ~ P y x -> exists z, P z y /\ ~ O z x.

已编写完成的证明脚本 #

Theorem extension : forall x y,
  (exists z, PP z x) -> (forall z, PP z x <-> PP z y) -> x = y.
Proof.
  intros x y [w PPwx] H.
  apply Peirce.
  intros Hcontra.
  destruct (classic (P y x)) as [yesP|notP].
  - pose proof (H y) as [].
    destruct H0.
    split; auto.
    contradiction.
  - pose proof (strong_supp x y notP) as [z []].
    assert (y = z).
    apply Peirce.
    intros Hcontra'.
    pose proof (H z) as [].
    destruct H3.
    split; auto.
    destruct H1.
    exists z.
    split.
    apply P_refl.
    assumption.
    rewrite <- H2 in H1.
    pose proof (H w) as [].
    pose proof (H3 PPwx).
    destruct PPwx.
    destruct H5.
    destruct H1.
    exists w.
    split; assumption.
Qed.

待解答疑问 #

我已经顺利完成了该证明，对此十分开心，但我认为当前证明脚本较为杂乱，不清楚该如何优化（我唯一想到的优化方向是使用模式匹配代替destruct策略）。
请问这个证明是否存在优化空间？如果可以优化，请不要使用过于复杂的策略，我希望能够理解你提出的所有优化点。

内容的提问来源于stack exchange，提问作者Lepticed