proposition: Lemma ideal_asym x y : ideal_leq x y -> ideal_leq y x -> x = y.
proof: Proof. move: x y=>[x1 H1][x2 H2]; rewrite /ideal_leq /= => H3 H4; move: H1 H2. rewrite (poset_asym H3 H4)=>H1 H2. congr Ideal; apply: proof_irrelevance. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype) LemmaOverloading(rels prelude)