Lemma stn_ne_iff_neq {n : nat} (i j: ⟦n⟧ ) : ¬ (i = j) <-> stntonat _ i ≠ stntonat _ j. Proof. intros. split. - intro ne. apply nat_nopath_to_neq. Set Printing Coercions. idtac. intro e; apply ne; clear ne. apply subtypePath_prop. assumption. - simpl. intros neq e. apply (nat_neq_to_nopath neq), maponpaths. assumption. Unset Printing Coercions. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.