Require Import Prelude.

Section WO.
  Variables (X : Type) (R : X -> X -> Prop).
  Notation "x <= y" := (R x y).
  Notation "x < y" := (x <= y /\ x <> y).
  Variable XM : forall P, P \/ ~ P.

  Inductive Acc : X -> Prop :=
  |AccI x : (forall y, y < x -> Acc y) -> Acc x.

  Fact inacc x :
    ~ Acc x -> exists y, y < x /\ ~ Acc y.
  Proof.
    intros H. contra XM H1. contradict H.
    constructor. intros y H2. contra XM H3.
    contradict H1. now exists y.
  Qed.

  Definition regular p := ex p -> exists x, p x /\ forall z, p z -> x <= z.

  Variable anti : forall x y, x <= y -> y <= x -> x = y.
  Variable linear : forall x y, x <= y \/ y <= x.

  Fact acc_regular :
    all Acc <-> all regular.
  Proof.
    split.
    - intros H1 p (x&H2).
      induction (H1 x) as [x _ IH].
      destruct (XM (exists y, y < x /\ p y)) as [(y&H3&H4)|H3].
      + now apply (IH y).
      + exists x. split. exact H2.
        intros z H4. contra XM H5.
        contradict H3. exists z. split; [|exact H4].
        destruct (linear z x) as [H6|H6].
        * split. exact H6. intros ->. apply H5, H6.
        * contradict H5. exact H6.
    - intros H x. contra XM H1.
      destruct (H (fun z => ~ Acc z)) as (y&H2&H3).
      + now exists x.
      + apply inacc in H2 as (z&(H4&H5)&H6).
        specialize (H3 z H6).
        destruct (anti H3 H4). now apply H5.
  Qed.

End WO.