proposition: Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
proof: Proof. intros n m (q & r & H). apply gcd_unique; trivial using divide_1_l, le_0_1. intros p Hn Hm. rewrite <- H. apply divide_add_r; now apply divide_mul_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd