proposition: Lemma zlt_diffP a b: intp a -> intp b -> (a <z b <-> inc (b -z a) BZps).
proof: Proof. move => pa pb; split. move => [/(zle_diffP pa pb)] pc pd; apply /BZps_iP;split => //. dneg aux; symmetry; exact (BZdiff_diag_rw pb pa aux). move /BZps_iP => [] /(zle_diffP pa pb) pc pd; split => //. by dneg aux; rewrite aux (BZdiff_diag pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)