Lemma isStrongOrder_reverse {X : UU} (l : hrel X) : isStrongOrder l → isStrongOrder (hrel_reverse l). Proof. intros H. repeat split. - apply istrans_reverse, (istrans_isStrongOrder H). - apply iscotrans_reverse,(iscotrans_isStrongOrder H). - apply isirrefl_reverse, (isirrefl_isStrongOrder H). Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.