proposition: Theorem L_Euclides : forall x a b : nat, is_gcd x a 1 -> divides x (a * b) -> divides x b.
proof: Proof. intros x a b H' H'0; replace b with (b * gcd x a). apply preEuclid; auto with arith. exists b; auto with arith. rewrite Nat.mul_comm; auto. rewrite (is_gcd_unic x a (gcd x a) 1); auto with arith. apply gcd_is_gcd; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)