Definition of InLeft and InRight
The page you reference for Coq defines inLeft and inRight as constructors of the inductive type sumor. The names themselves come from "left/right injection", as in the left/right injection into a sum type. Other names commonly used are inl/inr, Left/Right, $\iota_0$/$\iota_1$, and variations on these (e.g. that Coq file also defines left/right in the definition of sumbool). It also defines inl/inr as the constructors of the general sum type. sum, sumor, and sumbool are minor, technical variations of each other.

Which terms are used depends on the author, but they are most commonly used for injections into a sum type, particularly in a type theory/category theory context. Of course, an author is always free to use them for something else if they provide a definition.