proposition: Lemma BZsum_AC x y z: intp x -> intp y -> intp z -> (x +z y) +z z = (x +z z) +z y.
proof: Proof. move => xz yz zz. by rewrite - (BZsumA xz yz zz) - (BZsumA xz zz yz) (BZsumC y). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)