proposition: Lemma isaset_submonoid (A : monoid) : isaset (submonoid A).
proof: Proof. apply isaset_total2. - apply isasethsubtype. - intro P. apply isasetaprop, isapropissubmonoid. Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders