From 55136b24e757d322e570a9370eb48a0b14a1d320 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 1 Nov 2017 18:40:23 +0100
Subject: [PATCH] Add a comment regarding the use of `Topped`

---
 FiniteSets/misc/ordered.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/FiniteSets/misc/ordered.v b/FiniteSets/misc/ordered.v
index 46ab730..20981ec 100644
--- a/FiniteSets/misc/ordered.v
+++ b/FiniteSets/misc/ordered.v
@@ -155,6 +155,7 @@ Section min_set.
   Context `{TotalOrder A}.
   Context `{Univalence} `{IsHSet A}.
 
+  (* The reason why we put an additional element on top, is so that we can take the minimum of two results when considering union *)
   Definition min_set : FSet A -> Topped A.
   Proof.
     hrecursion.