proposition: Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
proof: Proof. fix gcd_greatest 1. intros [|a] b; simpl; auto. fold (b mod (S a)). intros c H H'. apply gcd_greatest; auto. set (a':=S a) in *. rewrite (div_mod_eq b a') in H'. destruct H as (u,Hu), H' as (v,Hv). exists (v - (b/a')*u). rewrite mul_comm in Hv. rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu. now rewrite add_comm, add_sub. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass