proposition: Lemma BZgcd_sum a b: intp a -> intp b -> BZgcd a (b +z a) = BZgcd a b.
proof: Proof. move => az bz; move: (BZgcd_rem az bz ZS1). by rewrite (BZprod_1r az). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)