coq - Coq: 非公式な証明を形式化するのに役立ちます

Question

Theorem ev_ev__ev_full : forall n m,
  even (n+m) <-> (even n <-> even m).
Proof.
  intros n m. split.
  - intros H. split.
    + intros H1. apply (ev_ev__ev n m H H1).
    + intros H1. rewrite plus_comm in H. apply (ev_ev__ev m n H H1).
  - intros H.

出力：

  n, m : nat
  H : even n <-> even m
  ============================
  even (n + m)

n は偶数でも非偶数でもかまいません。

• n が偶数の場合、m も偶数です。定理によりev_sum(n+m) も偶数です。

• n が偶数でない場合は、(n' + 1) の形式になります。n' は偶数です。m も偶数ではなく、(m' + 1) の形をしています。ここで、m' は偶数です。したがって、それらの合計は次のようになります。

  n + m = n' + 1 + m' + 1 => n + m = (n' + m') + 2.

偶数 ((n' + m') + 2)。( n apply ev_SS' + m') になったら。n' が偶数で m' が偶数であることがわかっているので、apply ev_sum. そして、これは定理を証明します。

この非公式な証明を coq でどのように記述しますか?