Library hydras.solutions_exercises.lt_succ_le

From hydras Require Import OrdinalNotations.ON_Generic.
From Coq Require Import Relations.

Section Proofs_of_lt_succ_le.

Context (A:Type)
        (lt : relation A)
        (cmp : Compare A)
        (On : ON lt cmp).

Section Proofs.
  Variables alpha beta : A.

beta is a successor of alpha

  Hypothesis Halphabeta : Successor beta alpha.

  Section S1.
  Variable gamma: A.
  Hypothesis HGammaBeta : lt gamma beta.

  Lemma L1: leq lt gamma alpha.

  End S1.

End Proofs.

End Proofs_of_lt_succ_le.