proposition: Proposition isaprop_is_monotone {X₁ X₂ : hSet} (R₁ : PartialOrder X₁) (R₂ : PartialOrder X₂) (f : X₁ → X₂) : isaprop (is_monotone R₁ R₂ f).
proof: Proof. repeat (use impred ; intro). apply (pr1 R₂). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics