proposition: Proposition is_monotone_lower_set_setquot_pr : is_monotone RX quotient_lower_set (setquotpr _).
proof: Proof. intros x₁ x₂ p. apply hinhpr ; cbn. exact (inr p). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.Posets.PointedPosets