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. apply divide_add_cancel_r with (r*m). - now apply divide_mul_r. - rewrite add_comm, <- H. now apply divide_mul_r. Qed.
imports: NAxioms NSub NZGcd