possible copy/paste errors in 07_Euclidean_Algorithm.lean

[ketilwright]

There is a theorem gcd_dvd starting about line 60 of this file. It's not clear if the reader should resolve the 8 sorries or not. I think not since gcd_dvd_right & left come next.

In any case: Following the split_ifs with h1 h2 . . ., and preceding each "sorry", is the comment "prove that gcd a b | b" (or | a).

In no case does the comment reflect the current goal. For example, the first goal is gcd b (fmod a b) ∣ b, the next is gcd b (fmod a b) ∣ a, etc,