proposition: Lemma BZopp_positive1 x: inc x BZps -> inc (BZopp x) BZms.
proof: Proof. move /BZps_iP => [pa pb]; move: (BZp_sg pa)(BZp_sBZ pa) => h1 h2. apply: (BZms_i (ZSo h2)) (proj2 (BZopp_sg h2 pb) h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)