Definition from_maybe {X : UU} (m : maybe X) (p : m != nothing) : X. Proof. unfold nothing in p. destruct m as [x | u]. - exact x. - contradiction p. now induction u. 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.