proposition: Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
proof: Proof. rewrite -modz_abs /gcdz; move/absz: m => m. have [-> | m_gt0] := posnP m; first by rewrite modz0. case: n => n; first by rewrite modz_nat gcdn_modr. rewrite modNz_nat // NegzE abszN {2}(divn_eq n m) -addnS gcdnMDl. rewrite -addrA -opprD -intS /=; set m1 := _.+1. have le_m1m: (m1 <= m)%N by apply: ltn_pmod. by rewrite subzn // !(gcdnC m) -{2 3}(subnK le_m1m) gcdnDl gcdnDr gcdnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)