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