diff options
| -rw-r--r-- | theories/Structures/OrdersTac.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index 408348139d..1c8073972d 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -100,9 +100,9 @@ Definition interp_ord o := match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end. Local Notation "#" := interp_ord. -Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z. +Lemma trans o o' x y z : #o x y -> #o' y z -> #(o+o') x z. Proof. -destruct o, o'; simpl; intros x y z; +destruct o, o'; simpl; rewrite ?P.le_lteq; intuition auto; subst_eqns; eauto using (StrictOrder_Transitive x y z) with *. Qed. |