proposition: Lemma gcd_lincomb_nat_dec : forall x y d : nat, x > 0 -> Zis_gcd (Z.of_nat x) (Z.of_nat y) (Z.of_nat d) -> {a : Z * Z | Z.of_nat d = (Z.of_nat x * fst a + Z.of_nat y * snd a)%Z}.
proof: Proof. intro x; apply (lt_wf_rec x); intros X IH. intros y d H H0. elim (div_eucl X H y). intro z; elim z. intros q r; clear z; simpl in |- *. case r. - intros; induction p as (H1, H2). rewrite <- plus_n_O in H1. exists (1%Z, 0%Z). simpl fst; simpl snd. rewrite <- Zmult_0_r_reverse; rewrite <- Zplus_0_r_reverse. rewrite Z.mul_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 Zis_gcd_sym; assumption. constructor. + exists 0%Z. auto. + exists 1%Z. lia. + auto. - intros r1 [H1 H2]. elim (IH (S r1) H2 X d). + intro z; elim z. intros delta gamma; clear z. simpl fst; simpl snd. intros p. exists ((gamma - Z.of_nat q * delta)%Z, delta). simpl fst; simpl snd. rewrite p, H1. 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 (Z.mul_assoc (Z.of_nat X)). rewrite (Z.mul_comm (Z.of_nat X) (- Z.of_nat q)). rewrite Zopp_mult_distr_l_reverse. rewrite Zopp_mult_distr_l_reverse. rewrite <- (Z.add_assoc (Z.of_nat X * gamma)). rewrite <- Znat.inj_mult. rewrite (Z.add_assoc (- (Z.of_nat (q * X) * delta))). rewrite Zplus_opp_l. simpl in |- *. apply Z.add_comm. + auto with arith. + apply (euclid_gcd1 d (Z.of_nat y) (Z.of_nat X) (Z.of_nat q) (Z.of_nat (S r1))). * apply Zis_gcd_sym; assumption. * rewrite <- Znat.inj_mult; rewrite <- Znat.inj_plus; apply Znat.inj_eq; assumption. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow