Library hydras.solutions_exercises.predSuccUnicity
From hydras Require Import OrdinalNotations.ON_Generic.
From Coq Require Import Relations.
Section Proofs_of_unicity.
Context (A:Type)
(lt le : relation A)
(cmp : Compare A)
(On : ON lt cmp).
Section Proofs.
Variables alpha beta : A.
From Coq Require Import Relations.
Section Proofs_of_unicity.
Context (A:Type)
(lt le : 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 Halphagamma : Successor gamma alpha.
Lemma L1 : gamma = beta.
End S1.
Section S2.
Variable gamma: A.
Hypothesis Hgammaalpha : Successor beta gamma.
Lemma L2 : gamma = alpha.
End S2.
End Proofs.
Please remind that Successor beta alpha must be read as
"beta is a successor of alpha"