proposition: Proposition isPartialOrder_discrete_hrel : isPartialOrder discrete_hrel.
proof: Proof. refine ((_ ,, _) ,, _). - intros x y z p q. exact (p @ q). - exact (λ x, idpath _). - exact (λ x y p q, p). Qed.
imports: UniMath.MoreFoundations.All