proposition: Theorem ischoicebasestn ( n : nat ) : ischoicebase (⟦n⟧).
proof: Proof. induction n as [ | n IHn ]. - apply ( ischoicebaseempty2 negstn0 ). - apply ( ischoicebaseweqf ( weqdnicoprod n lastelement ) ( ischoicebasecoprod IHn ischoicebaseunit ) ). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions