proposition: Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
proof: Proof. fix gcd_divide 1. intros [|a] b; simpl. - split. + now exists 0. + exists 1; simpl. now rewrite <- plus_n_O. - fold (b mod (S a)). destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). set (a':=S a) in *. split; auto. rewrite (div_mod_eq b a') at 2. destruct H as (u,Hu), H' as (v,Hv). rewrite mul_comm. exists ((b/a')*v + u). rewrite mul_add_distr_r. now rewrite <- mul_assoc, <- Hv, <- Hu. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass