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