proposition: Lemma stn_ne_iff_neq {n : nat} (i j: ⟦n⟧ ) : ¬ (i = j) <-> stntonat _ i ≠ stntonat _ j.
proof: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions