proposition: Lemma preEuclid : forall a b c m : nat, divides c (m * a) -> divides c (m * b) -> divides c (m * gcd a b).
proof: Proof. intros a b; pattern a, b in |- *; apply gcd_ind; clear a b. intros x c m H' H'0; rewrite gcd_def0l; auto. intros x c m H' H'0; rewrite gcd_def0r; auto. intros a b H' c m H'0 H'1; rewrite <- gcd_def2. apply H'; auto. apply divides_plus2 with (m * a); auto. replace (m * a + m * b) with (m * (b + a)); auto with arith; ring. intros a b H' c m H'0 H'1; rewrite <- gcd_def3. apply H'; auto. apply divides_plus2 with (m * b); auto. replace (m * b + m * a) with (m * (a + b)); auto with arith; ring. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)