proposition: Lemma BZpsS_lcm x y: inc x BZps -> inc y BZps -> inc (BZlcm x y) BZps.
proof: Proof. move => xs ys. move /BZps_iP: (xs) => [pa xnz]; move: (BZp_sBZ pa) => xz. move /BZps_iP: (ys) => [pb ynz]; move: (BZp_sBZ pb) => yz. apply /BZps_iP; split; last by apply: (BZlcm_nz xz yz xnz ynz). rewrite /BZlcm; apply: ZpS_quo; last by apply: ZpS_gcd. by apply: ZpS_prod. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)