Q:

what does the colon greater than sign mean in coq

For example 
Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.

what does the ":>" mean?
I hope this isn't a duplicate, but a symbol is hard to search for.

A:

In this particular case it inserts a Coercion from the posreal record to its field pos. This means you can use a posreal for an R in most cases.
Try:
Definition idR (x : R) := x.
Variable (r : posreal).
Compute (idR r).

See https://coq.inria.fr/refman/Reference-Manual021.html#Coercions-and-records

