proposition: Lemma bezout_sc p q a b m : a*p+b*q = 1 + m -> p div m \/ q div m -> is_gcd p q 1.
proof: Proof. intros H1 H2; do 2 (split; auto). intros k H4 H5. apply divides_plus_inv with m. + destruct H2 as [ H2 | H2 ]; apply divides_trans with (2 := H2); auto. + rewrite Nat.add_comm, <- H1. apply divides_plus; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)