Stuck at a simple inequality of natural number proof in Coq

I want to prove the inversion of inequality on negation, in natural numbers:

forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.

I attempt to prove by induction. I first trivially prove that w - i >= w - i by reflexity. Then I try to prove w - i >= w - S m provided that w - i >= w - m, and I get stuck. It seems that if I prove w - m >= w - S m, it's done. But I can't solve that either. Could anyone help? Thank you so much!

Why isn't there an easy list of available tactics alongside their descriptions on the web?

I'm no expert at this, but a way you can structure this proof in Coq:

Require Import Arith.

Lemma le_minus : forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j.
Proof.
  intros i j H1 w H2 H3.
  (* Induction on j *)
  induction j as [| m IHm].
  - (* Base Case: j = 0 *)
    assert (i = 0) as Hi0 by lia.
    rewrite Hi0. simpl. auto.
  - (* Inductive Step: j = S m *)
    destruct (Nat.eq_dec i (S m)).
    + (* Case: i = S m *)
      subst. lia.
    + (* Case: i < S m *)
      assert (i <= m) as H4 by lia.
      specialize (IHm H4 w H2).
      apply le_trans with (w - m). 
      * apply IHm. lia.
      * simpl. lia.
Qed.

Base Case

If j = 0, then by the condition i ≤ j, we have i = 0. The goal is w − 0 ≥ w − 0, which is trivial.

Inductive Step j = S m

• We assume the hypothesis i ≤ m (i.e., w − i ≥ w − m) holds.
• Now, we need to prove w − i ≥ w − S m.
• We do a case analysis on whether i = S m or i < S m.
• If i = S m, then w − i ≥ w − j is trivial since w − S m ≥ w - S m.
• If i < S m, we use the induction hypothesis to reduce the goal and then apply basic arithmetic reasoning.

Tactics

• intros: Introduces the quantified variables and assumptions.
• induction j as [| m IHm]: Performs induction on jj.
• destruct (Nat.eq_dec i (S m)): Case analysis on whether i = S m or i < S m.
• assert (i = 0) as Hi0 by lia: Introduces and proves a necessary equality using the lia tactic.
• lia: A powerful tactic that solves linear arithmetic goals.
• apply le_trans: Uses the transitivity of ≥≥ to combine results.

Some useful Coq tactics resources on the web

• https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html
• https://coq.inria.fr/doc/V8.19.2/refman/proof-engine/tactics.html
• https://www.inf.ed.ac.uk/teaching/courses/tspl/cheatsheet.pdf
• https://julesjacobs.com/notes/coq-cheatsheet/coq-cheatsheet.pdf

Unfortunately, there is no "easy" list of Coq tactics out there on the web, and it does require quite a digging online.

I hope this helps!