Trigonometric simplification for distance on a sphere
These are two equivalent equations for distance on a sphere:
hav(x)=sin(x/2)^2 dist1(lat1, lat2, dLon)=2*asin(hav(lat1-lat2)+cos(lat1)*cos(lat2)*hav(dLon)) dist2(lat1, lat2, dLon)=acos(sin(lat1)*sin(lat2)+cos(lat1)*cos(lat2)*cos(dLon))
(According to http://www.movable-type.co.uk/scripts... ) Indeed numerically they evaluate equal.
But why their difference does not simplify to 0?
Am I doing something wrong? Is there a way to have Sage prove the two forms are equivalent, or to transform one to another?