Definition stn_compl {n : nat} (i: ⟦n⟧ ) := compl_ne _ i (stnneq i).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.