proposition: Theorem bezout_comm : forall a b g, b ~= 0 -> Bezout a b g -> Bezout b a g.
proof: Proof. intros a b g Hb [p [q Hpq]]. destruct (eq_decidable a 0) as [Ha|Ha]. { exists 0, 0. symmetry in Hpq. rewrite Ha, mul_0_r in Hpq. apply eq_add_0 in Hpq as [-> _]. now nzsimpl. } exists (a*(p+1)*(q+1)-q), (b*(p+1)*(q+1)-p). enough (E' : (a*(p+1)*(q+1)-q+q)*b == (b*(p+1)*(q+1)-p+p)*a). { rewrite (mul_add_distr_r _ _ a), (mul_add_distr_r _ _ b), Hpq in E'. rewrite add_assoc, (add_comm _ g) in E'. now apply add_cancel_r in E'. } rewrite !sub_add. - now rewrite !(mul_comm _ b), !mul_assoc, !(mul_comm _ a), !mul_assoc. - rewrite <- mul_1_r at 1. apply mul_le_mono; [|apply le_add_l]. rewrite <- mul_1_l at 1. apply mul_le_mono; [|apply le_add_r]. rewrite one_succ. apply le_succ_l. assert (H := le_0_l b). order. - rewrite <- mul_1_l at 1. apply mul_le_mono; [|apply le_add_r]. rewrite <- mul_1_l at 1. apply mul_le_mono; [|apply le_add_l]. rewrite one_succ. apply le_succ_l. assert (H := le_0_l a). order. Qed.
imports: NAxioms NSub NZGcd