proposition: Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) -> exists q r, n == q*r /\ (q | m) /\ (r | p).
proof: Proof. intros n m p Hn H. assert (G := gcd_nonneg n m). le_elim G. - destruct (gcd_divide_l n m) as (q,Hq). exists (gcd n m). exists q. split. + now rewrite mul_comm. + split. * apply gcd_divide_r. * destruct (gcd_divide_r n m) as (r,Hr). rewrite Hr in H. rewrite Hq in H at 1. rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order]. apply gauss with r; trivial. apply mul_cancel_r with (gcd n m); [order|]. rewrite mul_1_l. rewrite <- gcd_mul_mono_r, <- Hq, <- Hr; order. - symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. Qed.
imports: NAxioms NSub NZGcd