proposition: Lemma meet_ge x y z : z <= x -> z <= y -> z <= meet x y.
proof: Proof. by move=> Hx Hy; apply: set_meetU_ge; rewrite set_meet1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)