(p : Prime) n : nat_gcd p n = 1 <-> ~ (p | n). Proof. split. - intros q [d r]. destruct r. rewrite (nat_gcd_r_add_r_mul p 0) in q. rewrite nat_gcd_zero_r in q. apply (@neq_iff_lt_or_gt p 1). 1: right; exact _. exact q. - intros nd. rapply nat_gcd_unique. intros q H1 H2. apply isprime in H1. destruct H1 as [H1|H1]. + destruct H1; exact _. + destruct H1; contradiction. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes