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