proposition: Lemma isStrongOrder_hnegispreorder : ∏ (X : hSet) (R : hrel X), isStrongOrder R → ispreorder (λ x y : X, (¬ R x y)%logic).
proof: 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.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets