proposition: Lemma bezout_rel_prime : forall a b:Z, Bezout a b 1 -> rel_prime a b.
proof: Proof. simple induction 1; intros ? ? H0; constructor; auto with zarith. intros. rewrite <- H0; auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat