proposition: Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p.
proof: Proof. assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)). { intros n Hn; pattern n. apply (fun H => strong_right_induction H 0); trivial. clear n Hn. intros n Hn IHn. apply le_lteq in Hn; destruct Hn as [Hn|Hn]. - intros m Hm; pattern m. apply (fun H => strong_right_induction H 0); trivial. clear m Hm. intros m Hm IHm. destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. + destruct (IHm (m-n)) as (a & b & EQ). * apply sub_nonneg; order. * now apply lt_sub_pos. * exists (a-b). exists b. rewrite gcd_sub_diag_r in EQ. rewrite <- EQ. rewrite mul_sub_distr_r, mul_sub_distr_l. now rewrite add_sub_assoc, add_sub_swap. + rewrite EQ. rewrite gcd_diag_nonneg; trivial. exists 1. exists 0. now nzsimpl. + destruct (IHn m Hm LT n) as (a & b & EQ). { order. } exists b. exists a. now rewrite gcd_comm, <- EQ, add_comm. - intros m Hm. rewrite <- Hn, gcd_0_l_nonneg; trivial. exists 0. exists 1. now nzsimpl. } assert (aux' : forall n m, 0<=m -> Bezout n m (gcd n m)). { intros n m Hm. destruct (le_ge_cases 0 n). - now apply aux. - assert (Hn' : 0 <= -n) by now apply opp_nonneg_nonpos. destruct (aux (-n) Hn' m Hm) as (a & b & EQ). exists (-a). exists b. now rewrite <- gcd_opp_l, <- EQ, mul_opp_r, mul_opp_l. } intros n m p Hp. rewrite <- Hp; clear Hp. destruct (le_ge_cases 0 m). - now apply aux'. - assert (Hm' : 0 <= -m) by now apply opp_nonneg_nonpos. destruct (aux' n (-m) Hm') as (a & b & EQ). exists a. exists (-b). now rewrite <- gcd_opp_r, <- EQ, mul_opp_r, mul_opp_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd