proposition: Proposition monotone_function_isPartialOrder : isPartialOrder monotone_function_order.
proof: Proof. simple refine ((_ ,, _) ,, _). - exact (λ f g h p q x, trans_PartialOrder RY (p x) (q x)). - exact (λ f x, refl_PartialOrder RY (pr1 f x)). - intros f g p q. use eq_monotone_function. intro x. exact (antisymm_PartialOrder RY (p x) (q x)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics