From 27b903865678b50ed17a8c783487a0871c220875 Mon Sep 17 00:00:00 2001
From: Eric Rodriguez <ericrboidi@gmail.com>
Date: Fri, 23 Sep 2022 17:34:02 +0000
Subject: [PATCH] feat(algebra/punit_instances):
 linear_ordered_add_comm_monoid_with_top punit (#16609)

---
 src/algebra/punit_instances.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/algebra/punit_instances.lean b/src/algebra/punit_instances.lean
index e0d96bc9658da..667a2a01d3f8d 100644
--- a/src/algebra/punit_instances.lean
+++ b/src/algebra/punit_instances.lean
@@ -80,6 +80,11 @@ instance : linear_ordered_cancel_add_comm_monoid punit :=
 { le_of_add_le_add_left := λ _ _ _ _, trivial,
   .. punit.canonically_ordered_add_monoid, ..punit.linear_order }
 
+instance : linear_ordered_add_comm_monoid_with_top punit :=
+{ top_add' := λ _, rfl,
+  ..punit.complete_boolean_algebra,
+  ..punit.linear_ordered_cancel_add_comm_monoid }
+
 instance : has_smul R punit :=
 { smul := λ _ _, star }