diff options
Diffstat (limited to 'theories/MSets/MSetInterface.v')
| -rw-r--r-- | theories/MSets/MSetInterface.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index a2a686d94d..ec432de83e 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -605,6 +605,10 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O. (** Specification of [lt] *) Instance lt_strorder : StrictOrder lt. + Proof. constructor ; unfold lt; red. + unfold complement. red. intros. apply (irreflexivity H). + intros. transitivity y; auto. + Qed. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. |