问如何证明所有关于le相等的证明？

EN

Import EqNotations.
Require Eqdep_dec PeanoNat.

Lemma nat_uip {x y : nat} (p q : x = y) : p = q.
apply Eqdep_dec.UIP_dec.
exact PeanoNat.Nat.eq_dec.
Qed.

(* Generalize le_ind to prove things about the proof *)
Lemma le_ind_dependent :
  forall (n : nat) (P : forall m : nat, n <= m -> Prop),
  P n (le_n n) ->
  (forall (m : nat) (p : n <= m), P m p -> P (S m) (le_S n m p)) ->
  forall (m : nat) (p : n <= m), P m p.
exact (fun n P Hn HS => fix ind m p : P m p := match p with
  | le_n _ => Hn | le_S _ m p => HS m p (ind m p) end).
Qed.

(*
Here we give an proof-by-cases principle for <= which keeps both the left
and right hand sides fixed.
*)
Lemma le_case_remember (x y : nat) (P : x <= y -> Prop)
  (IHn : forall (e : y = x), P (rew <- e in le_n x))
  (IHS : forall y' (q' : x <= y') (e : y = S y'), P (rew <- e in le_S x y' q'))
  : forall (p : x <= y), P p.
exact (fun p => match p with le_n _ => IHn | le_S _ y' q' => IHS y' q' end eq_refl).
Qed.

Theorem le_unique {x y : nat} (p q : x <= y) : p = q.
revert q.
induction p as [|y p IHp] using le_ind_dependent;
intro q;
case q as [e|x' q' e] using le_case_remember.

- rewrite (nat_uip e eq_refl).
  reflexivity.

- (* x = S x' but x <= x', so S x' <= x', which is a contradiction *)
  exfalso.
  rewrite e in q'.
  exact (PeanoNat.Nat.nle_succ_diag_l _ q').

- (* S y' = x but x <= y', so S y' <= y', which is a contradiction *)
  exfalso; clear IHp.
  rewrite <- e in p.
  exact (PeanoNat.Nat.nle_succ_diag_l _ p).

- injection e as e'.
  (* We now get rid of e as equal to (f_equal S e'), and then destruct e'
     now that it is an equation between variables. *)
  assert (f_equal S e' = e).
  + apply nat_uip.
  + destruct H.
    destruct e'.
    change (le_S x y p = le_S x y q').
    f_equal.
    apply IHp.

Qed.

(* Existing lemmas (e.g. Nat.le_exists_sub) seem unusable (declared opaque) *)
Fixpoint le_to_add {x y : nat} (prf : x <= y) : exists k, y = k + x :=
  match prf in _ <= y return exists k, y = k + x with
  | le_n _ => ex_intro _ 0 eq_refl
  | le_S _ y prf =>
    match le_to_add prf with
    | ex_intro _ k rec =>
      ex_intro
        _ (S k)
        match rec in _ = z return S y = S z with eq_refl => eq_refl end
    end
  end.
Fixpoint add_to_le (x k : nat) : x <= k + x :=
  match k with
  | O => le_n x
  | S k => le_S x (k + x) (add_to_le x k)
  end.
Theorem rebuild_le
  {x y : nat} (prf : x <= y)
: match le_to_add prf return x <= y with
  | ex_intro _ k prf =>
    match prf in _ = z return x <= z -> x <= y with
    | eq_refl => fun p => p
    end (add_to_le x k)
  end = prf.
Proof.
  revert y prf.
  fix rec 2. (* induction is not enough *)
  destruct prf as [ | y prf].
  - reflexivity.
  - specialize (rec y prf).
    simpl in *.
    destruct (le_to_add prf) as [k ->].
    subst prf.
    reflexivity.
Defined.

Theorem le_unique (x y : nat) (p q : x <= y) : p = q.
Proof.
  rewrite <- (rebuild_le p), <- (rebuild_le q).
  destruct (le_to_add p) as [k ->], (le_to_add q) as [l prf].
  pose proof (f_equal (fun n => n - x) prf) as prf'.
  simpl in prf'.
  rewrite ?Nat.add_sub in prf'.
  subst l.
  apply K_dec with (p := prf).
  + decide equality.
  + reflexivity.
Defined.