(p : Prime) n m : (p | n * m) -> (p | n) + (p | m). Proof. intros d. destruct (dec (p | n)) as [H|H]. 1: by left. right. apply nat_coprime_iff_not_divides in H. destruct (nat_bezout_pos_l p n _) as [x [y q]]. destruct H^; clear H. destruct d as [d r]. exists (x * m - y * d). lhs nrapply nat_dist_sub_r. rewrite <- 2 nat_mul_assoc. rewrite <- (nat_mul_comm p). destruct r^; clear r. rewrite 2 nat_mul_assoc. lhs_V nrapply nat_dist_sub_r. rhs_V nrapply nat_mul_one_l. apply (ap (fun x => nat_mul x m)). apply nat_moveR_nV. exact q. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes