Lemma dualelement_sn_le {m n k q: nat} (lt : S n < S k) : pr1 (dualelement (n,, lt)) <= (pr1 (dualelement (S n,, lt))). Proof. rewrite (@dualelement_sn_eq n n k k lt). apply isreflnatleh. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Maybe. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.Algebra.RigsAndRings.