proposition: Lemma BZ1_small c: inc c BZps -> \1z <=z c.
proof: Proof. move => h; move: (BZps_sBZ h) ZS1 => pa pb; split => //; constructor 3. move /indexed_P:h => [_ /setC1_P [pc pd] etc]. rewrite /BZ_one /BZ_of_nat /int_pp; aw; split => //; apply cge1; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)