proposition: Lemma stn_eq_or_neq_right {n} {i j : (⟦ n ⟧)%stn} : forall (p : i ≠ j), stn_eq_or_neq i j = inr p.
proof: Proof. intros; apply isaprop_stn_eq_or_neq. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings