diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-12 16:14:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-12 16:15:53 +0200 |
| commit | 63ff356a8546fbcb883bb6a9711c785f75fecd41 (patch) | |
| tree | 6f68842e0b1ded63a0ef96c11f18e08e33a360f5 /theories/Structures | |
| parent | 472914e8844387b756305eff0720fc8acb345d45 (diff) | |
Little addition to 6eede071 for consistency of style in OrdersFacts.v.
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 6f8fc1b32..0115d8a54 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -434,14 +434,14 @@ Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma ltb_compare x y : (x <? y) = match compare x y with Lt => true | _ => false end. Proof. apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff. -destruct compare; now split. +now destruct compare. Qed. Lemma leb_compare x y : |