proposition: Lemma Zgcd_minus : forall a b c, (a | c - b ) -> (Z.gcd a b | c).
proof: Proof. intros a b c (q,Hq). destruct (Zgcd_is_gcd a b) as [(a',Ha) (b',Hb) _]. set (g:=Z.gcd a b) in *; clearbody g. exists (q * a' + b'). symmetry in Hq. rewrite <- Z.add_move_r in Hq. rewrite <- Hq, Hb, Ha. ring. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory