Lemma isStrongOrder_hnegispreorder : ∏ (X : hSet) (R : hrel X), isStrongOrder R → ispreorder (λ x y : X, (¬ R x y)%logic). Proof. intros X R is. split. - intros x y z Hxy Hyz Hxz. generalize (iscotrans_isStrongOrder is _ y _ Hxz). apply toneghdisj. split. + exact Hxy. + exact Hyz. - exact (isirrefl_isStrongOrder is). Defined.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.