proposition: Lemma gcd_lincomb_nat : forall x y d : nat, x > 0 -> gcd (Z_of_nat x) (Z_of_nat y) d -> LinComb (Z_of_nat d) (Z_of_nat x) (Z_of_nat y).
proof: Proof. unfold LinComb in |- *. intro x. apply (lt_wf_ind x). intros X IH. intros. elim (div_rem X y). intro q. intros. elim H1. intro r. case r. intros. elim H2. intros. elim H4. intros. rewrite <- plus_n_O in H6. split with 1%Z. split with 0%Z. rewrite <- Zmult_0_r_reverse. rewrite <- Zplus_0_r_reverse. rewrite Zmult_comm. rewrite Zmult_1_l. apply Znat.inj_eq. apply (euclid_gcd d X (Z_of_nat y) (Z_of_nat X) (Z_of_nat q) 0). rewrite <- Zplus_0_r_reverse. rewrite <- Znat.inj_mult. apply Znat.inj_eq. assumption. apply gcd_sym. assumption. apply gcd_0_l. assumption. intro r1. intros. elim H2. intros. elim H4. intros. elim (IH (S r1) H5 X d). intro delta. intros. elim H7. intro gamma. intros. split with (gamma - Z_of_nat q * delta)%Z. split with delta. rewrite H6. rewrite H8. unfold Zminus in |- *. rewrite Zmult_plus_distr_r. rewrite Znat.inj_plus. rewrite Zmult_plus_distr_l. rewrite Znat.inj_mult. rewrite <- Zopp_mult_distr_l_reverse. rewrite (Zmult_assoc (Z_of_nat X)). rewrite (Zmult_comm (Z_of_nat X) (- Z_of_nat q)). rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse. rewrite (Zplus_assoc_reverse (Z_of_nat X * gamma)). rewrite <- Znat.inj_mult. rewrite (Zplus_assoc (- (Z_of_nat (q * X) * delta))). rewrite Zplus_opp_l. simpl in |- *. apply Zplus_comm. apply gt_Sn_O. apply (euclid_gcd1 d (Z_of_nat y) (Z_of_nat X) (Z_of_nat q) (Z_of_nat (S r1))). apply gcd_sym. assumption. rewrite <- Znat.inj_mult. rewrite <- Znat.inj_plus. apply Znat.inj_eq. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo