added to the hint

2020-02-01 14:36:58 -05:00 · 2020-02-01 14:36:58 -05:00 · 7c1d4d7903
commit 7c1d4d7903
parent c50f5713bc
1 changed files with 2 additions and 1 deletions
--- a/src/plfa/part1/Relations.lagda.md
+++ b/src/plfa/part1/Relations.lagda.md
@ -791,7 +791,8 @@ and back is the identity:
    to (from b) ≡ b

 (Hint: For each of these, you may first need to prove related
-properties of `One`.)
+properties of `One`. Also, you may need to prove that `1` is
+less or equal to the result of `from b`.)

 ```
 -- Your code goes here