From d9098ff4e504e49b974be8778894a3f561dbf654 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Wed, 8 Jul 2015 11:32:23 +1000
Subject: [PATCH] fix(library/theories/number_theory/bezout): make duplicate
 proof of prime -> irreducible an example

---
 library/theories/number_theory/bezout.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean
index 349a942e0..152f34c02 100644
--- a/library/theories/number_theory/bezout.lean
+++ b/library/theories/number_theory/bezout.lean
@@ -73,11 +73,15 @@ end
 
 end Bezout
 
+/-
+A sample application of Bezout's theorem, namely, an alternative proof that irreducible
+implies prime (dvd_or_dvd_of_prime_of_dvd_mul).
+-/
+
 namespace nat
 open int
 
-theorem dvd_or_dvd_of_dvd_mul_of_prime {p x y : ℕ} (pp : prime p) (H : p ∣ x * y) :
-  p ∣ x ∨ p ∣ y :=
+example {p x y : ℕ} (pp : prime p) (H : p ∣ x * y) : p ∣ x ∨ p ∣ y :=
 decidable.by_cases
   (assume Hpx : p ∣ x, or.inl Hpx)
   (assume Hnpx : ¬ p ∣ x,