proposition: Lemma gcd_bezout : forall n m, Bezout n m (gcd n m) \/ Bezout m n (gcd n m).
proof: Proof. intros n m. destruct (eq_0_gt_0_cases n) as [EQ|LT]. - right. rewrite EQ, gcd_0_l. exists 1. exists 0. now nzsimpl. - left. now apply gcd_bezout_pos. Qed.
imports: NAxioms NSub NZGcd