proposition: Lemma dualelement_sn_eq {m n k q: nat} (lt : S n < S k) : pr1 (dualelement (n,, lt)) = (pr1 (dualelement (S n,, lt))).
proof: Proof. do 2 rewrite dualelement_defs_eq; unfold dualelement'; simpl. now rewrite natminuseqn, natminusminus. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings