proposition: Lemma moduleiso'_to_moduleisweq_iso {R} (M N : module R) : isweq (moduleiso'_to_moduleiso M N).
proof: Proof. use (isweq_iso _ (moduleiso_to_moduleiso' M N)). - intro w. unfold moduleiso'_to_moduleiso, moduleiso_to_moduleiso'. cbn. induction w as [w1 w2]; cbn. use total2_paths_f; cbn. * use total2_paths_f; cbn. + reflexivity. + apply isapropismonoidfun. * apply isapropislinear. - reflexivity. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids