proposition: Lemma BZdvd_inf x y: inc x BZps -> inc y BZps -> inf BZdvdorder x y = BZgcd x y.
proof: Proof. move => xs ys; move: (BZdvd_lattice_aux xs ys) => [pa pb]. symmetry; apply: (infimum_pr2 BZdvdorder_or pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)