fact: Definition inr_monotone_function : monotone_function PY coproduct_PartialOrder := _ ,, is_monotone_inr.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions