diff --git a/server/nng/NNG/MyNat/LE.lean b/server/nng/NNG/MyNat/LE.lean
index 0e30011..7dc09cf 100644
--- a/server/nng/NNG/MyNat/LE.lean
+++ b/server/nng/NNG/MyNat/LE.lean
@@ -5,6 +5,9 @@ namespace MyNat
 def le (a b : ℕ) :=  ∃ (c : ℕ), b = a + c
 
 -- Another choice is to define it recursively: 
+-- note: I didn't choose this option because tests showed
+-- that mathematicians found it a lot more confusing than
+-- the existence definition.
 -- | le 0 _
 -- | le (succ a) (succ b) = le ab