Lemma stn_eq {k : nat} (i j : stn k) (eq : pr1 i = pr1 j) : i = j. Proof. now apply subtypePath_prop. 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.