diff --git a/doc/lean/calc.md b/doc/lean/calc.md
index 8a8674aae..5aa42857f 100644
--- a/doc/lean/calc.md
+++ b/doc/lean/calc.md
@@ -79,4 +79,6 @@ The Lean `let` construct can also be used to build calculational-like proofs.
              s2 : P a (f (f b))           :=   Subst s1 (Axf a),
              s3 : P a b                   :=   Subst s2 (Axf b)
          in s3.
-```
\ No newline at end of file
+```
+
+Finally, the [Nat (natural number) builtin library](../../src/builtin/Nat.lean) makes extensive use of calculational proofs.
\ No newline at end of file