proposition: Lemma isaprop_nat_eq_or_neq {m n : nat} : isaprop ((m = n) ⨿ (m ≠ n)).
proof: Proof. refine (@isaprop_dec_with_negProp (_,,_) (natneq _ _)). apply isasetnat. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings