Lemma isStrongOrder_setquot {X : UU} {R : eqrel X} {L : hrel X} (is : iscomprelrel R L) : isStrongOrder L → isStrongOrder (quotrel is). Proof. intros H. split ; [ | split]. - apply istransquotrel, (istrans_isStrongOrder H). - apply iscotransquotrel, (iscotrans_isStrongOrder H). - apply isirreflquotrel, (isirrefl_isStrongOrder H). Qed.
Require Import UniMath.MoreFoundations.Propositions. Require Import UniMath.MoreFoundations.Sets.