By Curry Howard correspondence, all theorems and lemmas are types and proof objects are values. As an example:
Theorem test: 0 <= 0.
Proof.
omega. Qed.
When I do, Check test. Coq's output is:
test
: 0 <= 0
But when I check the type of "<=", it is nat -> nat -> Prop. That means (0 <= 0) is of type Prop. Does this mean that the type 'test' is a subtype of Prop? In general, are theorem and lemma identifiers subtypes of Prop?
test : 0 <= 0 and 0 <= 0 : Prop, as you said. In the terminology of the Curry-Howard correspondence, 0 <= 0 is a type/theorem statement, and test is a value of that type/proof of that theorem.
There isn't any subtyping involved in this example. Subtyping is a relationship between two types; when Cat <: Animal (cat is a subtype of animal), it means all objects of type cat are also of type animal: x : Cat implies x : Animal.
Coq has one relatively simple form of subtyping, between type universes. The simplest example is that Prop is a subtype of Type. You can see this by using Check to confirm that 0 <= 0 : Prop and also 0 <= 0 : Type.