Le.lean

inductive Le (x : Nat) : (y : Nat) → Prop
  | refl : Le x x
  | step : Le x y → Le x y.succ

inductive Ge (x : Nat) : (y : Nat) → Prop
  | refl : Ge x x
  | step : Ge x y.succ → Ge x y

inductive Le' : (x y : Nat) → Prop
  | zero : Le' .zero y
  | succ : Le' x y → Le' x.succ y.succ

theorem Le.step' : Le x.succ y → Le x y
  | refl => step refl
  | step h => step (step' h)

theorem Le.zero : ∀ {y}, Le .zero y
  | .zero => refl
  | .succ _ => step zero

theorem Le.succ : Le x y → Le x.succ y.succ
  | refl => refl
  | step h => step (succ h)

theorem Ge.step' : Ge x y → Ge x.succ y
  | refl => step refl
  | step h => step (step' h)

theorem Ge.zero : ∀ {x}, Ge x .zero
  | .zero => refl
  | .succ _ => step' zero

theorem Ge.succ : Ge x y → Ge x.succ y.succ
  | refl => refl
  | step h => step (succ h)

theorem Le'.refl : ∀ {x}, Le' x x
  | .zero => zero
  | .succ _ => succ refl

theorem Le'.step : Le' x y → Le' x y.succ
  | zero => zero
  | succ h => succ (step h)

theorem Le'.step' : Le' x.succ y → Le' x y
  | succ h => step h