proposition: Lemma BZprod_Mltltge0 a b c d: inc a BZp -> inc c BZp -> a <z b -> c <z d -> (a *z c) <z (b *z d).
proof: Proof. move => pa pb pc pd. have H: (forall a b, inc a BZp -> a <z b -> inc b BZps). move => u v up uv; move: (uv) => [[uz vz _] _]. move/ (zlt_diffP uz vz): uv => pe; move: (ZpsS_sum_r up pe). by rewrite BZsum_diff. move: (H _ _ pa pc) (H _ _ pb pd) => bp cp. case: (equal_or_not c \0z) => cnz. by rewrite cnz BZprod_0r; apply /zlt0xP; apply: ZpsS_prod. by apply: BZprod_Mltltgt0 => //; apply/ BZps_iP;split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)