proposition: Lemma isStrongOrder_abgrdiff {X : abmonoid} (gt : hrel X) (Hgt : isbinophrel gt) : isStrongOrder gt → isStrongOrder (abgrdiffrel X Hgt).
proof: Proof. intros H. repeat split. - apply istransabgrdiffrel, (istrans_isStrongOrder H). - apply iscotransabgrdiffrel, (iscotrans_isStrongOrder H). - apply isirreflabgrdiffrel, (isirrefl_isStrongOrder H). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids