proposition: Lemma isaproparecompatibleactions {R S G} (mr : module_struct R G) (ms : module_struct S G) : isaprop (arecompatibleactions mr ms).
proof: Proof. apply (impredtwice 1); intros r s. apply (isofhlevelweqb 1 (Y := (module_mult (G,, mr) r ∘ module_mult (G,, ms) s ~ module_mult (G,, ms) s ∘ module_mult (G,, mr) r))). apply invweq. apply weqfunextsec. apply (impred 1); intros x. apply (pr2 (pr1 (pr1 G))). Defined.
imports: UniMath.Algebra.Modules.Core UniMath.Algebra.Groups UniMath.Algebra.Monoids UniMath.Algebra.RigsAndRings UniMath.Foundations.Preamble UniMath.Foundations.Sets