diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r-- | theories/Init/Datatypes.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index ddaf08bf7..11d80dbc3 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -262,6 +262,11 @@ Inductive comparison : Set := | Lt : comparison | Gt : comparison. +Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'. +Proof. + destruct c, c'; intro H; reflexivity || destruct H; discriminate. +Qed. + Definition CompOpp (r:comparison) := match r with | Eq => Eq @@ -326,7 +331,6 @@ Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, CompSpec eq lt x y c -> CompSpecT eq lt x y c. Proof. intros. apply CompareSpec2Type; assumption. Defined. - (******************************************************************) (** * Misc Other Datatypes *) |