Lemma dualelement_le_comp {n : nat} (i j : ⟦ n ⟧%stn) : i ≤ j -> (dualelement j) ≤ (dualelement i). Proof. intros le. destruct (natlehchoice i j) as [lt | eq]; try assumption. { apply natlthtoleh. apply (dualelement_lt_comp _ _ lt). } rewrite (stn_eq _ _ eq). apply isreflnatgeh. 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.