proposition: Lemma gcd_lincomb_pos : 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 y). intro. rewrite <- (inj_abs_pos x). rewrite <- (inj_abs_pos y). apply gcd_lincomb_nat. change (Z.abs_nat x > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. rewrite inj_abs_pos. rewrite inj_abs_pos. assumption. apply Z.le_ge. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. apply Z.le_ge. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. intro. rewrite <- (inj_abs_pos x). replace y with (- - y)%Z. rewrite <- (inj_abs_neg y). elim (gcd_lincomb_nat (Z.abs_nat x) (Z.abs_nat y) d). intro alpha. intros. elim H2. intro beta. intros. split with alpha. split with (- beta)%Z. rewrite <- Zopp_mult_distr_r. rewrite (Zmult_comm (- Z_of_nat (Z.abs_nat y))). rewrite <- Zopp_mult_distr_r. rewrite Z.opp_involutive. rewrite (Zmult_comm beta). assumption. change (Z.abs_nat x > Z.abs_nat 0) in |- *. apply gtzgt. apply Zlt_le_weak. apply Z.gt_lt. assumption. unfold Z.le in |- *. simpl in |- *. discriminate. assumption. rewrite inj_abs_pos. rewrite inj_abs_neg. apply gcd_opp_r. assumption. assumption. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. assumption. apply Z.opp_involutive. apply Z.le_ge. apply Zlt_le_weak. apply Z.gt_lt. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo