proposition: Lemma BZdiff_diff 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; rewrite /BZdiff. rewrite (BZoppD bq (ZSo cq)) (BZopp_K cq) BZsumA //; exact: ZSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)