add type signatures to theorems demonstrating naming conventions

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

Start at the identifiers-and-theorem-names section of the naming page and inspect each code block, beginning with the examples around mul_pos and add_lt_of_lt_of_nonpos. Check the examples in Lean 4 Web or locally, then add type-signature comments and naming explanations so the conventions remain understandable if theorem locations change.