Lemma isStrongOrder_abmonoidfrac {X : abmonoid} (Y : @submonoid X) (gt : hrel X) (Hgt : ispartbinophrel Y gt) : isStrongOrder gt → isStrongOrder (abmonoidfracrel X Y Hgt). Proof. intros H. split ; [ | split]. - apply istransabmonoidfracrel, (istrans_isStrongOrder H). - apply iscotransabmonoidfracrel, (iscotrans_isStrongOrder H). - apply isirreflabmonoidfracrel, (isirrefl_isStrongOrder H). Qed.
Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders. Require Import UniMath.Algebra.Monoids2.