I'm doing formal verification of the group properties of elliptic curve addition in Weiertrass form. I was taking as a reference this and this articles. The first does the verification for Weiertrass form and the second does it for Curve22519, a Montgomery curve, but his approach can be generalized to Weiertrass form.
My question is, can I proof the group properties for the Weiertrass form and then translate the operation from this form to Montgomery form or Edwards form? I believe the three of them present some "equivalent" families of curves. Would this approach preserve the good properties of each family?
For instance, say I do the verification for Weiertrass form and then I "convert" the results to Edwards form. Would this be still side-channel attacks resistant?