horizontal_sq_dtca[D:posreal] : THEORY
BEGIN

  IMPORTING vect_analysis@vect_deriv_2D[real],
            tangent_line[D]

  V    : VAR (differentiable_rv?)
  a,r  : VAR real
  s    : VAR Vect2
  ss   : VAR Ss_vect2
  pm   : VAR Sign

  horizontal_sq_dtca_diff : LEMMA
    (FORALL (a):nz_vect2?(V(a))) IMPLIES
    derivable?[real](LAMBDA (r: real): horizontal_sq_dtca(s, V(r)), r)

  horizontal_sq_dtca_deriv : LEMMA
    (FORALL (a):nz_vect2?(V(a))) IMPLIES
    deriv(LAMBDA(r:real):horizontal_sq_dtca(s,V(r)),r) = 
    LET v = V(r),
        w = deriv_rv(V)(r) IN
    (2*sqv(v)*det(s,v)*det(s,w)-2*sq(det(s,v))*(v*w))/sq(sqv(v))

  horizontal_sq_dtca_deriv_simpl : LEMMA
    (FORALL (a):nz_vect2?(V(a))) IMPLIES
    LET v = V(r),
        w = deriv_rv(V)(r) IN
    (2*sqv(v)*det(s,v)*det(s,w)-2*sq(det(s,v))*(v*w))/sq(sqv(v)) =
    2*det(s,v)*det(V(r),w)*(s*V(r))/sq(sqv(v))

  horizontal_sq_dtca_deriv_sign : LEMMA 
    (FORALL (a):nz_vect2?(V(a))) AND
    line_solution?(ss,V(r)) IMPLIES
    (pm*deriv(LAMBDA(r:real):horizontal_sq_dtca(ss,V(r)),r) > 0 IFF
     LET v   = V(r),
         w   = deriv_rv(V)(r),
         eps = eps_line(ss,v) IN
     pm*(Q(ss,eps)*w) > 0) 
  
END horizontal_sq_dtca