proposition: Lemma setP_lattice A: lattice (subp_order A).
proof: Proof. have [pa pb]:= (subp_osr A). split; [exact | rewrite pb]. move=> x y /setP_P xp /setP_P yp; split. by exists (x \cup y); apply: sup_inclusion. by exists (x \cap y); apply: inf_inclusion. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)