proposition: Lemma setP_lattice_d1 A: distributive_lattice1 (subp_order A).
proof: Proof. rewrite /distributive_lattice1 (proj2 (subp_osr A)) => x y z xA yA zA. rewrite (proj1 (setP_lattice_pr xA yA)) (proj1 (setP_lattice_pr xA zA)). rewrite (proj2 (setP_lattice_pr yA zA)). move: (xA)(yA)(zA) => /setP_P xA' /setP_P yA' /setP_P zA'. have yzA: inc (y \cap z) (\Po A) by apply/setP_P/subI2_set; left. have xyA: inc (x \cup y) (\Po A) by apply/setP_P/setU2_12S. have xzA: inc (x \cup z) (\Po A) by apply/setP_P/setU2_12S. rewrite (proj1 (setP_lattice_pr xA yzA)) (proj2 (setP_lattice_pr xyA xzA)). by rewrite set_UI2r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)