proposition: Lemma meet_le_r x y : meet x y <= y.
proof: Proof. move: (@set_meetUr (set1 x) (set1 y)); rewrite -lbP; exact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)