Definition dualelement_defs_eq {n : nat} (i : ⟦ n ⟧%stn) : dualelement i = dualelement' i. Proof. unfold dualelement', dualelement. apply subtypePath_prop; simpl. destruct (natchoice0 _) as [eq0 | gt]; reflexivity. 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.