The premiere dialectic in this area is Lakatos' "Proof and Refutations", which I highly recommend in general, and has plenty to say about the present topic. >

The premiere dialectic in this area is Lakatos' "Proof and Refutations", which I highly recommend in general, and has plenty to say about the present topic. > Q: Wait, where did "x" come from? A proof from intuition is not the same as a formal proof with an insightful step. I wager that many formal proofs (in Coq, say) would spur such "Wait, what is that for?" questions. In this case, the selection of some arbitrary non-zero real "x" is a creative step, not an intuitive one. The missing proviso that "x" is non-zero is an oversight, but it's a "small error", and -- with some experiential intuition -- can be recovered. (EDIT: The arbitrary variable is quickly overridden with a specific definition, but this is not typical unless there's a good reason to conceptualize it this way. If its value is obvious, define it up front and discuss why that value is the correct one.) > What if "d" is zero? This is (very nearly) a refutation, in the sense of Lakatos. We reflect and decide that our basic proof idea works for rectangles of positive area, and in some sense zero-area rectangles aren't really the objects we wanted to talk about. So we include this as an assumption. The digression about division by zero, inverses, etc. is valuable, but missing the point that this is an algebraic representation of a geometric problem. There's a lot that could be said about whether geometry is intuitive or formal, but I think the issue of divisibility by zero is side-stepping most of the interesting stuff. ...anyway, this is quite a convoluted proof. We assume a priori that for any rectangle R, its "area" A(R) is well-defined and computable. We'll assume that the rectangles are axis-aligned with side-lengths R.x and R.y for each axis. We could have a separate discussion and proof about the invariance of area under a change of basis. Theorem: Given a rectangle R with non-zero side-lengths R.x and R.y, and given a non-zero real number c, there exists a rectangle R2 with non-zero side-lengths where R2.x = c and A(R) = A(R2). Proof: Because R2.x is already specified, we need only determine R2.y. We know that, for rectangles, A(R) = R.x * R.y. So we desire that R.x * R.y = R2.x * R2.y. Because R2.x = c and c is non-zero, we have the equivalent desire that (R.x * R.y) / c = R2.y. Thus, the rectangle where R2.x = c and R2.y = (R.x * R.y) / c will have the same area as R and will have the desired side-length c. [] English? Yes. But it has more similarity with legalese than informal English. Each clause makes direct appeal to some rule of logic, and it could be transformed into a Coq proof (or any other proof assistant) without much ceremony.