proposition: Fact is_gcd_rel_prime p q g : is_gcd p q g -> exists a b, p = a*g /\ q = b*g /\ is_gcd a b 1.
proof: Proof. destruct (eq_nat_dec g 0) as [ H0 | H0 ]. * intros H; subst. apply is_gcd_0 in H; destruct H; subst. exists 1, 1 ; simpl; auto. * intros ((a & Ha) & (b & Hb) & H). exists a, b; repeat (split; auto). intros k H1 H2. destruct (H (k*g)) as (d & Hd); subst. + do 2 rewrite (Nat.mul_comm _ g); auto. + do 2 rewrite (Nat.mul_comm _ g); auto. + rewrite Nat.mul_assoc in Hd. replace g with (1*g) in Hd at 1 by (simpl; lia). apply Nat.mul_cancel_r in Hd; auto. symmetry in Hd. apply mult_is_one in Hd. destruct Hd; subst; auto. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)