Theorem: HTPI.Theorem_7_2_3 (HTPILib/Chap7.lean)

State before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
⊢ p ∣ a ∨ p ∣ b
Tactic:
or_right with h3
State after:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
⊢ p ∣ b

State before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
⊢ p ∣ b
Tactic:
have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3
State after:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
h4 : rel_prime a p
⊢ p ∣ b

State before:
a b p : ℕ
h1 : prime p
h2 : p ∣ a * b
h3 : ¬p ∣ a
h4 : rel_prime a p
⊢ p ∣ b
Tactic:
show p ∣ b from Theorem_7_2_2 h2 h4
State after:
no goals