proposition: Lemma BZdiff_diff2 a b c: intp a -> intp b -> intp c -> a -z (b +z c) = (a -z b) -z c.
proof: Proof. move => aq bq cq. by move:(BZdiff_diff aq bq (ZSo cq)); rewrite /BZdiff (BZopp_K cq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)