Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded

Yes, you edited your reply to be a lot less polite after you saw my reply to your reply, and I don’t think I did anything to provoke that. I might’ve responded differently if I had realized you were in attack mode. Some points I’d like to clarify: 1. Multiple contradictory edits in the answer is weird by Stack Exchange standards regardless of the merits of the discussion, that’s the main thing I observed. 2. Whether Euclid uses contradiction or not is not really open to interpretation: the word “absurd” appears right in the proof. If people want to split hairs about whether that contradiction is in the lemma or the main proof, I guess fine. 3. There are of course multiple subschools of constructivism that accept and don’t accept different things. Not all of them ignore computational complexity. For example, some ultrafinitists reject the unique prime factorization theorem on the basis that you can’t really execute the factorization algorithm even for relatively modest numbers. To be clear, that’s not exactly my view, but I would for example agree that something like “just find the prime factors” sweeps a bit of relevant subtlety under the rug: you can only do that conceptually, not actually.