proposition: Lemma euclid_gcd1 : forall (d : nat) (x y q r : Z), gcd x y d -> x = (q * y + r)%Z -> gcd r y d.
proof: Proof. unfold gcd in |- *. unfold common_div in |- *. intros. elim H. intros. elim H1. intros. split. split. rewrite <- (abs_inj d). apply zdivdiv. apply zdiv_plus_r with (q * y)%Z. rewrite Zmult_comm. apply zdiv_mult_compat_l. apply divzdiv. rewrite abs_inj. assumption. rewrite <- H0. apply divzdiv. rewrite abs_inj. assumption. assumption. intros. elim H5. intros. apply H2. split. rewrite <- (abs_inj e). apply zdivdiv. rewrite H0. apply zdiv_plus_compat. rewrite Zmult_comm. apply zdiv_mult_compat_l. apply divzdiv. rewrite abs_inj. assumption. apply divzdiv. rewrite abs_inj. assumption. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo