Lemma isStrongOrder_abgrdiff {X : abmonoid} (gt : hrel X) (Hgt : isbinophrel gt) : isStrongOrder gt → isStrongOrder (abgrdiffrel X Hgt). Proof. intros H. repeat split. - apply istransabgrdiffrel, (istrans_isStrongOrder H). - apply iscotransabgrdiffrel, (iscotrans_isStrongOrder H). - apply isirreflabgrdiffrel, (isirrefl_isStrongOrder H). Qed.
Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.MoreFoundations.Subtypes.