proposition: Lemma isantisymmnegtoiscoantisymm {X : UU} {R : hrel X} (isdr : isdecrel R) (isr : isantisymmneg R) : iscoantisymm R.
proof: Proof. intros. intros x1 x2 nrx12. induction (isdr x2 x1) as [ r | nr ]. apply (ii1 r). apply ii2. apply (isr _ _ nrx12 nr). Defined.
imports: UniMath.Foundations.Propositions