proposition: Lemma meet_le x y : (x <= y) = (meet x y == x).
proof: Proof. apply/idP/idP => [Hxy|/eqP <-]; [|exact: meet_le_r]. by apply/eqP/le_anti; rewrite meet_le_l meet_ge. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop classical_sets)