proposition: Lemma isdeceqmaybe {X : UU} (dec : isdeceq X) : isdeceq (maybe X).
proof: Proof. apply isdeceqcoprod. - exact dec. - exact isdecequnit. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings