proposition: Lemma isStrongOrder_bck {X Y : UU} (f : Y → X) (gt : hrel X) : isStrongOrder gt → isStrongOrder (fun_hrel_comp f gt).
proof: Proof. intros is. split ; [ | split ]. - intros x y z. apply (istrans_isStrongOrder is). - intros x y z. apply (iscotrans_isStrongOrder is). - intros x. apply (isirrefl_isStrongOrder is). Qed.
imports: UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Sets