Lemma isaprop_stn_eq_or_neq {n} (i j : ⟦n⟧%stn) : isaprop ((i = j) ⨿ (i ≠ j)). Proof. refine (@isaprop_dec_with_negProp (_,,_) (stnneq _ _)). apply isasetstn. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.