proposition: Lemma logeqabgrdiffrelints (X : abmonoid) (L : hrel X) : hrellogeq (abgrdiffrelint' X L) (abgrdiffrelint X L).
proof: Proof. split. unfold abgrdiffrelint. unfold abgrdiffrelint'. simpl. apply hinhfun. intro t2. set (a0 := pr1 (pr1 t2)). split with a0. apply (pr2 t2). simpl. apply hinhfun. intro t2. set (x0 := pr1 t2). split with (tpair _ x0 tt). apply (pr2 t2). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids