如何用归纳法在Coq中证明引理forall x y, x<=y -> div2 x <= div2 y？

首先定义div2（若环境未自带）：

Fixpoint div2 (n : nat) : nat :=
  match n with
  | O => O
  | S O => O
  | S (S n') => S (div2 n')
  end.

第一步：证明辅助引理：div2是弱递增的 #

即对任意自然数n，div2 n <= div2 (S n)：

Lemma div2_le_S : forall n, div2 n <= div2 (S n).
Proof.
  induction n as [ | n'].
  - (* n = 0 *) simpl. reflexivity.
  - (* n = S n' *) destruct n' as [ | n''].
    + (* n' = 0，即n=1 *) simpl. reflexivity.
    + (* n' = S n''，即n=2+n'' *) simpl.
      rewrite IHn'.
      apply le_S. reflexivity.
Qed.

第二步：对x<=y的归纳证明原引理 #

利用Coq中<=的归纳定义（le_n和le_S构造子）：

Lemma div2_monotone : forall x y, x <= y -> div2 x <= div2 y.
Proof.
  intros x y H.
  induction H.
  - (* 基础情况：x=y *) reflexivity.
  - (* 归纳步骤：x <= m 推出 x <= S m *)
    apply le_trans with (m := div2 m).
    + exact IHle.
    + apply div2_le_S.
Qed.

说明 #

单独对x或y归纳容易卡壳，因为div2的单调性和x<=y的构造逻辑绑定更紧密。对H: x<=y归纳直接贴合自然数<=的定义：要么x=y，要么y是某个满足x<=m的数的后继。归纳步骤中借助辅助引理的弱递增性，结合自然数<=的传递性le_trans，直接从归纳假设推导出结论。

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