proposition: Lemma dualelement_le_comp' {n : nat} (i j : ⟦ n ⟧%stn) : (dualelement i) ≤ (dualelement j) -> j ≤ i.
proof: Proof. intros le. pose (H := @dualelement_le_comp _ (dualelement i) (dualelement j) le). now do 2 rewrite dualelement_2x in H. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Maybe UniMath.Combinatorics.StandardFiniteSets UniMath.Algebra.Domains_and_Fields UniMath.Algebra.RigsAndRings