proposition: Lemma istransnegrel {X : UU} (R : hrel X) (isr : iscotrans R) : istrans (negrel R).
proof: Proof. intros. intros x1 x2 x3 r12 r23. apply (negf (isr x1 x2 x3)). apply (toneghdisj (make_dirprod r12 r23)). Defined.
imports: UniMath.Foundations.Propositions