proposition: Lemma nat_eq_or_neq_right {i j: nat} (p : i ≠ j) : nat_eq_or_neq i j = inr p.
proof: Proof. apply isaprop_nat_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