add type signatures to theorems demonstrating naming conventions

[JadAbouHawili]

In https://leanprover-community.github.io/contribute/naming.html#identifiers-and-theorem-names , the following section

import Mathlib.Algebra.Order.Monoid.Lemmas
import Mathlib.Algebra.Order.Ring.Lemmas

open Nat

#check mul_pos
#check mul_nonpos_of_nonneg_of_nonpos
#check add_lt_of_lt_of_nonpos
#check add_lt_of_nonpos_of_lt

doesn't run on Lean 4 Web and locally.

It would much more ideal to have comments with type signatures showing what the theorem is about and why it was given this name so that if things get moved around/break the ideas regarding naming conventions still come across.

The above is one code block from that page , a similar thing can be done for the other code blocks

[JadAbouHawili]

or even just import Mathlib for all the code blocks