proposition: Theorem gcd_lincomb : forall (x y : Z) (d : nat), x <> 0%Z -> gcd x y d -> LinComb (Z_of_nat d) x y.
proof: Proof. intros. elim (Zle_or_lt 0 x). intro. elim (Zle_lt_or_eq 0 x). intro. apply gcd_lincomb_pos. apply Z.lt_gt. assumption. assumption. intro. elim H. rewrite H2. reflexivity. assumption. intro. elim (gcd_lincomb_pos (- x) y d). intro alpha. intros. elim H2. intro beta. intros. split with (- alpha)%Z. split with beta. rewrite H3. rewrite (Zmult_comm x). rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse. rewrite (Zmult_comm alpha). reflexivity. apply Zopp_lt_gt_0. assumption. apply gcd_opp_l. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo