Even if binary relations and orders are a common formalization topic, we need to formalize specific orders (namely monomial and graded) in the process of formalizing in Rocq the finite element method. This article provides definitions, operators, and proofs of properties about relations and orders with a focus on monomial orders, that are total orders compatible with the monoid operation. More than its definition and proved properties, we define several of them, among them the lexicographic and grevlex orders. For the sake of genericity, we formalize the grading of an order, a high-level operator that transforms a binary relation into another one, and we prove that grading an order preserves many of its properties, such as the monomial order property. This leads us to the definition and properties of four different graded orders, with very factorized proofs. We therefore provide a comprehensive and user-friendly Rocq library about orders, including monomial and graded orders, that contains more than 700 lemmas.