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