proposition: Lemma zlt_diffP2 a b: intp a -> intp b -> (a <z b <-> inc (a -z b) BZms).
proof: Proof. move => pa pb; apply: (iff_trans (zlt_diffP pa pb)). rewrite - (BZoppB pb pa); split => h. by apply: BZopp_positive1. rewrite - (BZopp_K (ZS_diff pb pa)); apply: (BZopp_negative1 h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)