proposition: Lemma dualelement_le_comp {n : nat} (i j : ⟦ n ⟧%stn) : i ≤ j -> (dualelement j) ≤ (dualelement i).
proof: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings