proposition: Lemma issymm_stnneq {n : nat} {i j : stn n} (neq : i ≠ j) : (j ≠ i).
proof: Proof. apply issymm_natneq; assumption. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings