proofs /w equations for refl-style inductive leq on nats

prop_leq.v

From Equations Require Import Equations.
From Coq Require Import ssreflect ssrfun.
From mathcomp Require Import ssrnat.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive less_or_eq : nat -> nat -> Prop :=
| refl : forall {n k}, n = k -> less_or_eq n k
| step : forall {n k}, less_or_eq n k -> less_or_eq n k.+1.

Notation "n <<= m" := (less_or_eq n m) (at level 3).
Notation "n << m" := (less_or_eq n.+1 m) (at level 3).

Lemma leq0 n : 0 <<= n.
Proof.
elim: n; first by exact: refl.
by move=>n IH; apply: step.
Qed.

Lemma leqS n : n <<= n.+1.
Proof. by apply/step/refl. Qed.

Equations ltW n k : n << k -> n <<= k :=
ltW (refl erefl) => leqS _;
ltW (step p)     => step (ltW p).

Equations leqInj n k : n.+1 <<= k.+1 -> n <<= k :=
leqInj (refl erefl) => refl erefl;
leqInj (step p)     => ltW p.

Equations leqSS n k : n <<= k -> n.+1 <<= k.+1 :=
leqSS (refl erefl) => refl erefl;
leqSS (step p)     => step (leqSS p).

Equations leqV n k : n <<= k -> (n = k) \/ (n << k) :=
leqV (refl eq) => or_introl eq;
leqV (step p)  => or_intror (leqSS p).

Lemma n_ltS n : ~(n << n).
Proof.
elim: n=>/=.
- by move=>H; inversion H.
by move=>n IH /leqInj.
Qed.

Equations leq_trans n m p : n <<= m -> m <<= p -> n <<= p :=
leq_trans (refl erefl) p2 => p2;
leq_trans (step p1)    p2 => leq_trans p1 (ltW p2).

Equations leq_antisym n k : n <<= k -> k <<= n -> n = k :=
leq_antisym (refl eq) p2 => eq;
leq_antisym (step p1) p2 =>
  let pt := leq_antisym p1 (ltW p2) in
  ltac:(by move: (p2); rewrite pt => /n_ltS).

Lemma leq_total n m : n <<= m \/ m <<= n.
Proof.
elim: n; first by left; apply: leq0.
move=>n; case; last by move=>H; right; apply: step.
case/leqV; last by move=>H; left.
by move=>->; right; apply: leqS.
Qed.