proposition: Lemma BZdvd_lattice_aux x y: inc x BZps -> inc y BZps -> (least_upper_bound BZdvdorder (doubleton x y) (BZlcm x y) /\ (greatest_lower_bound BZdvdorder (doubleton x y) (BZgcd x y))).
proof: Proof. move: BZdvdorder_or => or. move: BZdvdorder_gle => H. move => xs ys. move: (BZpsS_gcd xs ys) (BZpsS_lcm xs ys) => gp lp. move:(BZps_sBZ xs) (BZps_sBZ ys) => xz yz. split. move: (BZlcm_prop2 xz yz) => [p1 p2 p3]. apply: (lub_set2 or); try apply /H => //. move => t; move/H => [_ ts ta]/H [_ _ tb]; move: (p3 _ ta tb) => tc. by apply/H. move: (BZgcd_prop3 xz yz) => [[p1 p2 p3] _]. apply: (glb_set2 or); last (move => t; move/H => [ts _ ta] /H [_ _ tb]; move: (p3 _ ta tb) => tc); by apply /H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)