Definition dualelement {n : nat} (i : ⟦n⟧ ) : ⟦n⟧. Proof. induction (natchoice0 n) as [H | H]. - exact (make_stn n (n - 1 - i) (fromempty (dualelement_0_empty i H))). - exact (make_stn n (n - 1 - i) (dualelement_lt i n H)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.