proposition: Lemma gcd_bezout_pos : forall n m, 0 < n -> Bezout n m (gcd n m).
proof: Proof. enough (H : forall nm, 0 < fst nm -> Bezout (fst nm) (snd nm) (gcd (fst nm) (snd nm))). { intros n m. apply (H (n, m)). } intros nm. induction nm as [[n m] IH] using (measure_induction _ (fun '(n, m) => n + m)). enough (H : forall n' m', n+m == n'+m' -> 0<n'<m' -> Bezout n' m' (gcd n' m')). { cbn. intros ?. destruct (lt_trichotomy n m) as [Hnm|[Hnm|Hnm]]. - now apply H. - exists 1, 0. now rewrite Hnm, mul_1_l, mul_0_l, add_0_r, gcd_diag. - destruct (eq_0_gt_0_cases m) as [->|?]. + exists 1, 0. now rewrite gcd_0_r, mul_1_l, mul_0_l, add_0_r. + apply bezout_comm; [order|]. rewrite gcd_comm. now apply H; [apply add_comm|]. } intros n' m' E' [Hn' Hn'm']. assert (Hlt : n' + (m' - n') < n + m). { rewrite (add_comm n'), E', sub_add by order. now apply lt_add_pos_l. } destruct (IH (n', m'-n') Hlt Hn') as [a [b Hab]]. cbn in Hab. exists (a+b), b. rewrite mul_add_distr_r, Hab, mul_sub_distr_l, gcd_sub_diag_r by order. now rewrite <- add_assoc, sub_add by (apply mul_le_mono_l; order). Qed.
imports: NAxioms NSub NZGcd