proposition: Lemma BZdvd_lattice: lattice BZdvdorder.
proof: Proof. split; first by apply: BZdvdorder_or. move => x y; rewrite BZdvdorder_sr => xs ys. move: (BZdvd_lattice_aux xs ys) => [pa pb]. split; [ by exists (BZlcm x y) | by exists (BZgcd x y) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)