proposition: Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
proof: Proof. intros n m p. apply gcd_unique_alt; try apply gcd_nonneg. intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. - apply divide_add_r; trivial. now apply divide_mul_r. - apply divide_add_cancel_r with (p*n); trivial. + now apply divide_mul_r. + now rewrite add_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd