fact: Definition moduleiso'_to_moduleweq_iso {R} (M N : module R) : (moduleiso' M N) ≃ (moduleiso M N) := make_weq (moduleiso'_to_moduleiso M N) (moduleiso'_to_moduleisweq_iso M N).
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids