Lemma iscotrans_to_istrans_negReln {X : UU} {R : hrel X} (NR : negReln R) : isdeccotrans R -> istrans NR. Proof. intros i ? ? ? nxy nyz. apply neg_to_negProp. apply (negf (i x1 x2 x3)). intro c. induction c as [c|c]. - exact (negProp_to_neg nxy c). - exact (negProp_to_neg nyz c). Defined.