# Kepler's Law

with(dtrisys): interface(prompt=`GEOTHER> `);
ord := [t,x,y,r,a]: depend(ord):
h1 := r^2-x^2-y^2:
h2 := a^2-df(x,2)^2-df(y,2)^2:
n1 := df(a*r^2):
n2 := df(x,2)*y-df(y,2)*x:  
hyp := {h1,h2,n1,n2}:
k1 := df(r,3)*(df(y,2)*df(x)-df(y)*df(x,2))
      +df(r,2)*(-df(y,3)*df(x)+df(y)*df(x,3))
      +df(r)*(df(y,3)*df(x,2)-df(y,2)*df(x,3)):
Kepler := dTheorem(hyp,k1,ord);

Remark(
`   For more details, see`,
`D. Wang: A Method for Proving Theorems in Differential Geometry and`,
`   Mechanics. J. Univ. Comput. Sci. 1 (1995): 658-673.`, 
`W.-t. Wu: Mechanical Theorem Proving of Differential Geometries and Some`,
`   of Its Applications in Mechanics. J. Automat. Reason.7 (1991): 171-191.` 
):
