content: {- This file is generated by Coq extraction mechanism (v7.4), and is modified to work (i.e. type-check) with hugs98 interpreter.
     The modification where merly renaming some coq constructors in order to avoid the clash with the hugs98 Prelude constructors 
     (which are automatically exported). At the end of the file some pretty printing functions are added by hand.
                                                                                 -- Milad Niqui
  -}
  
  
  
  module Quadratic where
  
  -- import qualified Prelude
  
  __ = error "Logical or arity value used"
  
  data Prod a b = Pair b a
  
  ffst p =
    case p of
      Pair x y -> x
  
  ssnd p =
    case p of
      Pair x y -> y
  
  false_rect _ =
    error "absurd case"
  
  false_rec _ =
    false_rect __
  
  and_rect f =
    f __ __
  
  and_rec f =
    and_rect f
  
  eq_rect x f y =
    f
  
  eq_rec x f y =
    eq_rect x f y
  
  eq_rec_r x h y =
    h
  
  data Sumbool = LLeft
                 | RRight
  
  sumbool_rect f f0 s =
    case s of
      LLeft -> f __
      RRight -> f0 __
  
  sumbool_rec f f0 s =
    sumbool_rect f f0 s
  
  data Sumor a = Inleft a
                 | Inright
  
  sumor_rect f f0 s =
    case s of
      Inleft x -> f x
      Inright -> f0 __
  
  sumor_rec f f0 s =
    sumor_rect f f0 s
  
  data Positive = XI Positive
                  | XO Positive
                  | XH  
  
  data Z = ZERO
           | POS Positive
           | NEG Positive 
  
  data Relation = EGAL
                  | INFERIEUR
                  | SUPERIEUR
  
  relation_rect f f0 f1 r =
    case r of
      EGAL -> f
      INFERIEUR -> f0
      SUPERIEUR -> f1
  
  relation_rec f f0 f1 r =
    relation_rect f f0 f1 r
  
  add_un x =
    case x of
      XI x' -> XO (add_un x')
      XO x' -> XI x'
      XH -> XO XH
  
  add x y =
    case x of
      XI x' ->
        (case y of
           XI y' -> XO (add_carry x' y')
           XO y' -> XI (add x' y')
           XH -> XO (add_un x'))
      XO x' ->
        (case y of
           XI y' -> XI (add x' y')
           XO y' -> XO (add x' y')
           XH -> XI x')
      XH ->
        (case y of
           XI y' -> XO (add_un y')
           XO y' -> XI y'
           XH -> XO XH)
  
  add_carry x y =
    case x of
      XI x' ->
        (case y of
           XI y' -> XI (add_carry x' y')
           XO y' -> XO (add_carry x' y')
           XH -> XI (add_un x'))
      XO x' ->
        (case y of
           XI y' -> XO (add_carry x' y')
           XO y' -> XI (add x' y')
           XH -> XO (add_un x'))
      XH ->
        (case y of
           XI y' -> XI (add_un y')
           XO y' -> XO (add_un y')
           XH -> XI XH)
  
  double_moins_un x =
    case x of
      XI x' -> XI (XO x')
      XO x' -> XI (double_moins_un x')
      XH -> XH
  
  ccompare x y r =
    case x of
      XI x' ->
        (case y of
           XI y' -> ccompare x' y' r
           XO y' -> ccompare x' y' SUPERIEUR
           XH -> SUPERIEUR)
      XO x' ->
        (case y of
           XI y' -> ccompare x' y' INFERIEUR
           XO y' -> ccompare x' y' r
           XH -> SUPERIEUR)
      XH -> (case y of
               XI y' -> INFERIEUR
               XO y' -> INFERIEUR
               XH -> r)
  
  data Entier = Nul
                | Pos Positive
  
  un_suivi_de x =
    case x of
      Nul -> Pos XH
      Pos p -> Pos (XI p)
  
  zero_suivi_de x =
    case x of
      Nul -> Nul
      Pos p -> Pos (XO p)
  
  double_moins_deux x =
    case x of
      XI x' -> Pos (XO (XO x'))
      XO x' -> Pos (XO (double_moins_un x'))
      XH -> Nul
  
  sub_pos x y =
    case x of
      XI x' ->
        (case y of
           XI y' -> zero_suivi_de (sub_pos x' y')
           XO y' -> un_suivi_de (sub_pos x' y')
           XH -> Pos (XO x'))
      XO x' ->
        (case y of
           XI y' -> un_suivi_de (sub_neg x' y')
           XO y' -> zero_suivi_de (sub_pos x' y')
           XH -> Pos (double_moins_un x'))
      XH ->
        (case y of
           XI y' -> Pos (double_moins_un y')
           XO y' -> double_moins_deux y'
           XH -> Nul)
  
  sub_neg x y =
    case x of
      XI x' ->
        (case y of
           XI y' -> un_suivi_de (sub_neg x' y')
           XO y' -> zero_suivi_de (sub_pos x' y')
           XH -> Pos (double_moins_un x'))
      XO x' ->
        (case y of
           XI y' -> zero_suivi_de (sub_neg x' y')
           XO y' -> un_suivi_de (sub_neg x' y')
           XH -> double_moins_deux x')
      XH ->
        (case y of
           XI y' -> Pos (XO y')
           XO y' -> Pos (double_moins_un y')
           XH -> Nul)
  
  op r =
    case r of
      EGAL -> EGAL
      INFERIEUR -> SUPERIEUR
      SUPERIEUR -> INFERIEUR
  
  zplus x y =
    let true_sub = \x0 y0 -> case sub_pos x0 y0 of
                               Nul -> XH
                               Pos z -> z
    in
    (case x of
       ZERO -> y
       POS x' ->
         (case y of
            ZERO -> x
            POS y' -> POS (add x' y')
            NEG y' ->
              (case ccompare x' y' EGAL of
                 EGAL -> ZERO
                 INFERIEUR -> NEG (true_sub y' x')
                 SUPERIEUR -> POS (true_sub x' y')))
       NEG x' ->
         (case y of
            ZERO -> x
            POS y' ->
              (case ccompare x' y' EGAL of
                 EGAL -> ZERO
                 INFERIEUR -> POS (true_sub y' x')
                 SUPERIEUR -> NEG (true_sub x' y'))
            NEG y' -> NEG (add x' y')))
  
  zopp x =
    case x of
      ZERO -> ZERO
      POS x0 -> NEG x0
      NEG x0 -> POS x0
  
  times x y =
    case x of
      XI x' -> add y (XO (times x' y))
      XO x' -> XO (times x' y)
      XH -> y
  
  zmult x y =
    case x of
      ZERO -> ZERO
      POS x' ->
        (case y of
           ZERO -> ZERO
           POS y' -> POS (times x' y')
           NEG y' -> NEG (times x' y'))
      NEG x' ->
        (case y of
           ZERO -> ZERO
           POS y' -> NEG (times x' y')
           NEG y' -> POS (times x' y'))
  
  zccompare x y =
    case x of
      ZERO ->
        (case y of
           ZERO -> EGAL
           POS y' -> INFERIEUR
           NEG y' -> SUPERIEUR)
      POS x' ->
        (case y of
           ZERO -> SUPERIEUR
           POS y' -> ccompare x' y' EGAL
           NEG y' -> SUPERIEUR)
      NEG x' ->
        (case y of
           ZERO -> INFERIEUR
           POS y' -> INFERIEUR
           NEG y' -> op (ccompare x' y' EGAL))
  
  zsgn z =
    case z of
      ZERO -> ZERO
      POS p -> POS XH
      NEG p -> NEG XH
  
  zabs z =
    case z of
      ZERO -> ZERO
      POS p -> POS p
      NEG p -> POS p
  
  zminus m n =
    zplus m (zopp n)
  
  dccompare_inf r =
    relation_rec (Inleft LLeft) (Inleft RRight) Inright r
  
  zccompare_rec x y h1 h2 h3 =
    sumor_rec (\h -> sumbool_rec h1 h2 h) h3
      (dccompare_inf (zccompare x y))
  
  z_eq_dec x y =
    zccompare_rec x y (\_ -> LLeft) (\_ -> RRight) (\_ -> RRight)
  
  z_lt_dec x y =
    zccompare_rec x y (\_ -> RRight) (\_ -> LLeft) (\_ -> RRight)
  
  z_le_dec x y =
    zccompare_rec x y (\_ -> LLeft) (\_ -> LLeft) (\_ -> RRight)
  
  z_lt_ge_dec x y =
    z_lt_dec x y
  
  z_le_lt_eq_dec x y =
    zccompare_rec x y (\_ -> RRight) (\_ -> LLeft) (\_ -> false_rec __)
  
  z_zerop x =
    z_eq_dec x ZERO
  
  data Qpositive = NR Qpositive
                   | DL Qpositive
                   | One 
  
  qpositive_rect f f0 f1 q =
    case q of
      NR q0 -> f q0 (qpositive_rect f f0 f1 q0)
      DL q0 -> f0 q0 (qpositive_rect f f0 f1 q0)
      One -> f1
  
  qpositive_rec f f0 f1 q =
    qpositive_rect f f0 f1 q
  
  data Q = Zero
           | Qpos Qpositive
           | Qneg Qpositive 
  
  qpositive_eq_dec w w' =
    qpositive_rec (\q h w'0 ->
      case w'0 of
        NR w'1 -> sumbool_rec (\_ -> LLeft) (\_ -> RRight) (h w'1)
        DL q0 -> RRight
        One -> RRight) (\q h w'0 ->
      case w'0 of
        NR q0 -> RRight
        DL w'1 -> sumbool_rec (\_ -> LLeft) (\_ -> RRight) (h w'1)
        One -> RRight) (\w'0 ->
      case w'0 of
        NR q -> RRight
        DL q -> RRight
        One -> LLeft) w w'
  
  not_Zeq_inf x y =
    case z_lt_ge_dec x y of
      LLeft -> LLeft
      RRight ->
        (case z_le_lt_eq_dec y x of
           LLeft -> RRight
           RRight -> false_rec __)
  
  z_dec x y =
    case z_lt_ge_dec x y of
      LLeft -> Inleft LLeft
      RRight ->
        (case z_le_lt_eq_dec y x of
           LLeft -> Inleft RRight
           RRight -> Inright)
  
  z_dec' x y =
    case z_eq_dec x y of
      LLeft -> Inright
      RRight -> Inleft (not_Zeq_inf x y)
  
  z_lt_le_dec x y =
    z_lt_ge_dec x y
  
  quadro_leq_inf a b c d =
    case z_lt_le_dec a c of
      LLeft -> RRight
      RRight -> (case z_lt_le_dec b d of
                  LLeft -> RRight
                  RRight -> LLeft)
  
  zsgn_1 x =
    case x of
      ZERO -> Inleft LLeft
      POS p -> Inleft RRight
      NEG p -> Inright
  
  encoding_algorithm x y =
    case z_dec' x y of
      Inleft h_x_neq_y ->
        (case h_x_neq_y of
           LLeft -> DL (encoding_algorithm x (zminus y x))
           RRight -> NR (encoding_algorithm (zminus x y) y))
      Inright -> One
  
  positive_fraction_encoding x y =
    encoding_algorithm x y
  
  fraction_encoding m n =
    case z_dec (zmult (zsgn m) (zsgn n)) ZERO of
      Inleft s0 ->
        (case s0 of
           LLeft -> Qneg (positive_fraction_encoding (zabs m) (zabs n))
           RRight -> Qpos (positive_fraction_encoding (zabs m) (zabs n)))
      Inright -> Zero
  
  outside_interval a b =
    zplus (zsgn a) (zsgn b)
  
  inside_interval_1_dec_inf_subproof o1 o2 =
    case z_lt_dec ZERO o1 of
      LLeft -> z_lt_dec ZERO o2
      RRight ->
        (case z_lt_dec o1 ZERO of
           LLeft -> z_lt_dec o2 ZERO
           RRight -> RRight)
  
  inside_interval_1_dec_inf o1 o2 =
    inside_interval_1_dec_inf_subproof o1 o2
  
  inside_interval_2_dec_inf_subproof o1 o2 =
    case z_lt_dec ZERO o1 of
      LLeft -> z_lt_dec o2 ZERO
      RRight ->
        (case z_lt_dec o1 ZERO of
           LLeft -> z_lt_dec ZERO o2
           RRight -> RRight)
  
  inside_interval_2_dec_inf o1 o2 =
    inside_interval_2_dec_inf_subproof o1 o2
  
  qhomographic_sign a b c d p =
    let o1 = outside_interval a b in
    let o2 = outside_interval c d in
    (case p of
       NR q ->
         (case z_zerop b of
            LLeft ->
              (case z_zerop d of
                 LLeft -> Pair (zmult (zsgn a) (zsgn c)) (Pair (Pair a
                   (Pair b (Pair c d))) (NR q))
                 RRight ->
                   (case z_lt_dec ZERO o2 of
                      LLeft -> Pair (zsgn a) (Pair (Pair a (Pair b (Pair c
                        d))) (NR q))
                      RRight ->
                        (case z_lt_dec o2 ZERO of
                           LLeft -> Pair (zopp (zsgn a)) (Pair (Pair a
                             (Pair b (Pair c d))) (NR q))
                           RRight ->
                             qhomographic_sign a (zplus a b) c
                               (zplus c d) q)))
            RRight ->
              (case z_zerop d of
                 LLeft ->
                   (case z_lt_dec ZERO o1 of
                      LLeft -> Pair (zsgn c) (Pair (Pair a (Pair b (Pair c
                        d))) (NR q))
                      RRight ->
                        (case z_lt_dec o1 ZERO of
                           LLeft -> Pair (zopp (zsgn c)) (Pair (Pair a
                             (Pair b (Pair c d))) (NR q))
                           RRight ->
                             qhomographic_sign a (zplus a b) c
                               (zplus c d) q))
                 RRight ->
                   (case inside_interval_1_dec_inf o1 o2 of
                      LLeft -> Pair (POS XH) (Pair (Pair a (Pair b (Pair c
                        d))) (NR q))
                      RRight ->
                        (case inside_interval_2_dec_inf o1 o2 of
                           LLeft -> Pair (NEG XH) (Pair (Pair a (Pair b
                             (Pair c d))) (NR q))
                           RRight ->
                             qhomographic_sign a (zplus a b) c
                               (zplus c d) q))))
       DL q ->
         (case z_zerop b of
            LLeft ->
              (case z_zerop d of
                 LLeft -> Pair (zmult (zsgn a) (zsgn c)) (Pair (Pair a
                   (Pair b (Pair c d))) (DL q))
                 RRight ->
                   (case z_lt_dec ZERO o2 of
                      LLeft -> Pair (zsgn a) (Pair (Pair a (Pair b (Pair c
                        d))) (DL q))
                      RRight ->
                        (case z_lt_dec o2 ZERO of
                           LLeft -> Pair (zopp (zsgn a)) (Pair (Pair a
                             (Pair b (Pair c d))) (DL q))
                           RRight ->
                             qhomographic_sign (zplus a b) b (zplus c d)
                               d q)))
            RRight ->
              (case z_zerop d of
                 LLeft ->
                   (case z_lt_dec ZERO o1 of
                      LLeft -> Pair (zsgn c) (Pair (Pair a (Pair b (Pair c
                        d))) (DL q))
                      RRight ->
                        (case z_lt_dec o1 ZERO of
                           LLeft -> Pair (zopp (zsgn c)) (Pair (Pair a
                             (Pair b (Pair c d))) (DL q))
                           RRight ->
                             qhomographic_sign (zplus a b) b (zplus c d)
                               d q))
                 RRight ->
                   (case inside_interval_1_dec_inf o1 o2 of
                      LLeft -> Pair (POS XH) (Pair (Pair a (Pair b (Pair c
                        d))) (DL q))
                      RRight ->
                        (case inside_interval_2_dec_inf o1 o2 of
                           LLeft -> Pair (NEG XH) (Pair (Pair a (Pair b
                             (Pair c d))) (DL q))
                           RRight ->
                             qhomographic_sign (zplus a b) b (zplus c d)
                               d q))))
       One ->
         let soorat = zsgn (zplus a b) in
         (case z_eq_dec soorat ZERO of
            LLeft -> Pair ZERO (Pair (Pair a (Pair b (Pair c d))) One)
            RRight ->
              (case z_eq_dec soorat (zsgn (zplus c d)) of
                 LLeft -> Pair (POS XH) (Pair (Pair a (Pair b (Pair c d)))
                   One)
                 RRight -> Pair (NEG XH) (Pair (Pair a (Pair b (Pair c
                   d))) One))))
  
  sg_sign a b c d qp =
    case qp of
      NR q ->
        (case z_zerop b of
           LLeft ->
             (case z_zerop d of
                LLeft ->
                  eq_rec_r (Pair (zmult (zsgn a) (zsgn c)) (Pair (Pair a
                    (Pair b (Pair c d))) (NR q)))
                    (case a of
                       ZERO -> Inleft LLeft
                       POS pa ->
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inleft RRight
                            NEG pc -> Inright)
                       NEG pa ->
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inright
                            NEG pc -> Inleft RRight))
                    (qhomographic_sign a b c d (NR q))
                RRight ->
                  (case z_lt_dec ZERO (outside_interval c d) of
                     LLeft ->
                       eq_rec_r (Pair (zsgn a) (Pair (Pair a (Pair b
                         (Pair c d))) (NR q)))
                         (case a of
                            ZERO -> Inleft LLeft
                            POS pa -> Inleft RRight
                            NEG pa -> Inright)
                         (qhomographic_sign a b c d (NR q))
                     RRight ->
                       (case z_lt_dec (outside_interval c d) ZERO of
                          LLeft ->
                            eq_rec_r (Pair (zopp (zsgn a)) (Pair (Pair a
                              (Pair b (Pair c d))) (NR q)))
                              (case a of
                                 ZERO -> Inleft LLeft
                                 POS pa -> Inright
                                 NEG pa -> Inleft RRight)
                              (qhomographic_sign a b c d (NR q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign a (zplus a b) c
                                (zplus c d) q)
                              (sg_sign a (zplus a b) c (zplus c d) q)
                              (qhomographic_sign a b c d (NR q)))))
           RRight ->
             (case z_zerop d of
                LLeft ->
                  (case z_lt_dec ZERO (outside_interval a b) of
                     LLeft ->
                       eq_rec_r (Pair (zsgn c) (Pair (Pair a (Pair b
                         (Pair c d))) (NR q)))
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inleft RRight
                            NEG pc -> Inright)
                         (qhomographic_sign a b c d (NR q))
                     RRight ->
                       (case z_lt_dec (outside_interval a b) ZERO of
                          LLeft ->
                            eq_rec_r (Pair (zopp (zsgn c)) (Pair (Pair a
                              (Pair b (Pair c d))) (NR q)))
                              (case c of
                                 ZERO -> Inleft LLeft
                                 POS pc -> Inright
                                 NEG pc -> Inleft RRight)
                              (qhomographic_sign a b c d (NR q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign a (zplus a b) c
                                (zplus c d) q)
                              (sg_sign a (zplus a b) c (zplus c d) q)
                              (qhomographic_sign a b c d (NR q))))
                RRight ->
                  (case inside_interval_1_dec_inf (outside_interval a b)
                          (outside_interval c d) of
                     LLeft ->
                       eq_rec_r (Pair (POS XH) (Pair (Pair a (Pair b
                         (Pair c d))) (NR q))) (Inleft RRight)
                         (qhomographic_sign a b c d (NR q))
                     RRight ->
                       (case inside_interval_2_dec_inf
                               (outside_interval a b)
                               (outside_interval c d) of
                          LLeft ->
                            eq_rec_r (Pair (NEG XH) (Pair (Pair a (Pair b
                              (Pair c d))) (NR q))) Inright
                              (qhomographic_sign a b c d (NR q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign a (zplus a b) c
                                (zplus c d) q)
                              (sg_sign a (zplus a b) c (zplus c d) q)
                              (qhomographic_sign a b c d (NR q))))))
      DL q ->
        (case z_zerop b of
           LLeft ->
             (case z_zerop d of
                LLeft ->
                  eq_rec_r (Pair (zmult (zsgn a) (zsgn c)) (Pair (Pair a
                    (Pair b (Pair c d))) (DL q)))
                    (case a of
                       ZERO -> Inleft LLeft
                       POS pa ->
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inleft RRight
                            NEG pc -> Inright)
                       NEG pa ->
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inright
                            NEG pc -> Inleft RRight))
                    (qhomographic_sign a b c d (DL q))
                RRight ->
                  (case z_lt_dec ZERO (outside_interval c d) of
                     LLeft ->
                       eq_rec_r (Pair (zsgn a) (Pair (Pair a (Pair b
                         (Pair c d))) (DL q)))
                         (case a of
                            ZERO -> Inleft LLeft
                            POS pa -> Inleft RRight
                            NEG pa -> Inright)
                         (qhomographic_sign a b c d (DL q))
                     RRight ->
                       (case z_lt_dec (outside_interval c d) ZERO of
                          LLeft ->
                            eq_rec_r (Pair (zopp (zsgn a)) (Pair (Pair a
                              (Pair b (Pair c d))) (DL q)))
                              (case a of
                                 ZERO -> Inleft LLeft
                                 POS pa -> Inright
                                 NEG pa -> Inleft RRight)
                              (qhomographic_sign a b c d (DL q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign (zplus a b) b
                                (zplus c d) d q)
                              (sg_sign (zplus a b) b (zplus c d) d q)
                              (qhomographic_sign a b c d (DL q)))))
           RRight ->
             (case z_zerop d of
                LLeft ->
                  (case z_lt_dec ZERO (outside_interval a b) of
                     LLeft ->
                       eq_rec_r (Pair (zsgn c) (Pair (Pair a (Pair b
                         (Pair c d))) (DL q)))
                         (case c of
                            ZERO -> Inleft LLeft
                            POS pc -> Inleft RRight
                            NEG pc -> Inright)
                         (qhomographic_sign a b c d (DL q))
                     RRight ->
                       (case z_lt_dec (outside_interval a b) ZERO of
                          LLeft ->
                            eq_rec_r (Pair (zopp (zsgn c)) (Pair (Pair a
                              (Pair b (Pair c d))) (DL q)))
                              (case c of
                                 ZERO -> Inleft LLeft
                                 POS pc -> Inright
                                 NEG pc -> Inleft RRight)
                              (qhomographic_sign a b c d (DL q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign (zplus a b) b
                                (zplus c d) d q)
                              (sg_sign (zplus a b) b (zplus c d) d q)
                              (qhomographic_sign a b c d (DL q))))
                RRight ->
                  (case inside_interval_1_dec_inf (outside_interval a b)
                          (outside_interval c d) of
                     LLeft ->
                       eq_rec_r (Pair (POS XH) (Pair (Pair a (Pair b
                         (Pair c d))) (DL q))) (Inleft RRight)
                         (qhomographic_sign a b c d (DL q))
                     RRight ->
                       (case inside_interval_2_dec_inf
                               (outside_interval a b)
                               (outside_interval c d) of
                          LLeft ->
                            eq_rec_r (Pair (NEG XH) (Pair (Pair a (Pair b
                              (Pair c d))) (DL q))) Inright
                              (qhomographic_sign a b c d (DL q))
                          RRight ->
                            eq_rec_r
                              (qhomographic_sign (zplus a b) b
                                (zplus c d) d q)
                              (sg_sign (zplus a b) b (zplus c d) d q)
                              (qhomographic_sign a b c d (DL q))))))
      One ->
        (case z_eq_dec (zsgn (zplus a b)) ZERO of
           LLeft ->
             eq_rec_r (Pair ZERO (Pair (Pair a (Pair b (Pair c d))) One))
               (Inleft LLeft) (qhomographic_sign a b c d One)
           RRight ->
             (case z_eq_dec (zsgn (zplus a b)) (zsgn (zplus c d)) of
                LLeft ->
                  eq_rec_r (Pair (POS XH) (Pair (Pair a (Pair b (Pair c
                    d))) One)) (Inleft RRight)
                    (qhomographic_sign a b c d One)
                RRight ->
                  eq_rec_r (Pair (NEG XH) (Pair (Pair a (Pair b (Pair c
                    d))) One)) Inright (qhomographic_sign a b c d One)))
  
  h_sign a b c d p =
    case qhomographic_sign a b c d p of
      Pair l1 l2 -> l1
  
  sg_sign_dec a b c d p =
    sg_sign a b c d p
  
  qpositive_dec_One p =
    qpositive_eq_dec p One
  
  top_more_informative a b c d =
    case quadro_leq_inf a b c d of
      LLeft ->
        and_rec (\_ _ ->
          case z_le_lt_eq_dec c a of
            LLeft -> LLeft
            RRight -> z_le_lt_eq_dec d b)
      RRight -> RRight
  
  qhomographic_Qpositive_to_Qpositive a b c d p =
    case qpositive_dec_One p of
      LLeft -> positive_fraction_encoding (zplus a b) (zplus c d)
      RRight ->
        (case top_more_informative a b c d of
           LLeft -> NR
             (qhomographic_Qpositive_to_Qpositive (zminus a c)
               (zminus b d) c d p)
           RRight ->
             (case top_more_informative c d a b of
                LLeft -> DL
                  (qhomographic_Qpositive_to_Qpositive a b (zminus c a)
                    (zminus d b) p)
                RRight ->
                  (case p of
                     NR q ->
                       qhomographic_Qpositive_to_Qpositive a (zplus a b)
                         c (zplus c d) q
                     DL q ->
                       qhomographic_Qpositive_to_Qpositive (zplus a b) b
                         (zplus c d) d q
                     One -> false_rec __)))
  
  new_a a b c d p =
    ffst (ffst (ssnd (qhomographic_sign a b c d p)))
  
  new_b a b c d p =
    ffst (ssnd (ffst (ssnd (qhomographic_sign a b c d p))))
  
  new_c a b c d p =
    ffst (ssnd (ssnd (ffst (ssnd (qhomographic_sign a b c d p)))))
  
  new_d a b c d p =
    ssnd (ssnd (ssnd (ffst (ssnd (qhomographic_sign a b c d p)))))
  
  new_p a b c d p =
    ssnd (ssnd (qhomographic_sign a b c d p))
  
  qhomographic_Qpositive_to_Q a b c d p =
    case z_eq_dec (zmult a d) (zmult b c) of
      LLeft ->
        (case z_zerop d of
           LLeft -> fraction_encoding a c
           RRight -> fraction_encoding b d)
      RRight ->
        (case sg_sign_dec a b c d p of
           Inleft l1_not_minus_one ->
             (case l1_not_minus_one of
                LLeft -> Zero
                RRight ->
                  (case z_lt_le_dec ZERO
                          (zsgn
                            (zplus (new_a a b c d p) (new_b a b c d p))) of
                     LLeft -> Qpos
                       (qhomographic_Qpositive_to_Qpositive
                         (new_a a b c d p) (new_b a b c d p)
                         (new_c a b c d p) (new_d a b c d p)
                         (new_p a b c d p))
                     RRight -> Qpos
                       (qhomographic_Qpositive_to_Qpositive
                         (zopp (new_a a b c d p))
                         (zopp (new_b a b c d p))
                         (zopp (new_c a b c d p))
                         (zopp (new_d a b c d p)) (new_p a b c d p))))
           Inright ->
             (case z_lt_le_dec
                     (zsgn (zplus (new_a a b c d p) (new_b a b c d p)))
                     ZERO of
                LLeft -> Qneg
                  (qhomographic_Qpositive_to_Qpositive
                    (zopp (new_a a b c d p)) (zopp (new_b a b c d p))
                    (new_c a b c d p) (new_d a b c d p)
                    (new_p a b c d p))
                RRight -> Qneg
                  (qhomographic_Qpositive_to_Qpositive (new_a a b c d p)
                    (new_b a b c d p) (zopp (new_c a b c d p))
                    (zopp (new_d a b c d p)) (new_p a b c d p))))
  
  qhomographic a b c d s =
    case s of
      Zero -> fraction_encoding b d
      Qpos p -> qhomographic_Qpositive_to_Q a b c d p
      Qneg p -> qhomographic_Qpositive_to_Q (zopp a) b (zopp c) d p
  
  outside_square a b c d =
    zplus (zplus (zplus (zsgn a) (zsgn b)) (zsgn c)) (zsgn d)
  
  three_integers_dec_inf a b c =
    case z_zerop a of
      LLeft -> (case z_zerop b of
                 LLeft -> z_zerop c
                 RRight -> RRight)
      RRight -> RRight
  
  inside_square_1_dec_inf o1 o2 =
    case z_lt_dec (POS (XO XH)) o1 of
      LLeft -> z_lt_dec (POS (XO XH)) o2
      RRight ->
        (case z_lt_dec o1 (NEG (XO XH)) of
           LLeft -> z_lt_dec o2 (NEG (XO XH))
           RRight -> RRight)
  
  inside_square_2_dec_inf o1 o2 =
    case z_lt_dec (POS (XO XH)) o1 of
      LLeft -> z_lt_dec o2 (NEG (XO XH))
      RRight ->
        (case z_lt_dec o1 (NEG (XO XH)) of
           LLeft -> z_lt_dec (POS (XO XH)) o2
           RRight -> RRight)
  
  qquadratic_sign a b c d e f g h p1 p2 =
    let o1 = outside_square a b c d in
    let o2 = outside_square e f g h in
    (case p1 of
       NR xs ->
         (case p2 of
            NR ys ->
              (case three_integers_dec_inf b c d of
                 LLeft ->
                   (case three_integers_dec_inf f g h of
                      LLeft -> Pair (zmult (zsgn a) (zsgn e)) (Pair (Pair
                        (Pair a (Pair b (Pair c d))) (Pair e (Pair f
                        (Pair g h)))) (Pair (NR xs) (NR ys)))
                      RRight ->
                        (case z_lt_dec (POS (XO XH)) o2 of
                           LLeft -> Pair (zsgn a) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (NR ys)))
                           RRight ->
                             (case z_lt_dec o2 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn a)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (NR xs) (NR
                                  ys)))
                                RRight ->
                                  qquadratic_sign a (zplus a b)
                                    (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) e
                                    (zplus e f) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) xs ys)))
                 RRight ->
                   (case three_integers_dec_inf f g h of
                      LLeft ->
                        (case z_lt_dec (POS (XO XH)) o1 of
                           LLeft -> Pair (zsgn e) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (NR ys)))
                           RRight ->
                             (case z_lt_dec o1 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn e)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (NR xs) (NR
                                  ys)))
                                RRight ->
                                  qquadratic_sign a (zplus a b)
                                    (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) e
                                    (zplus e f) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) xs ys))
                      RRight ->
                        (case inside_square_1_dec_inf o1 o2 of
                           LLeft -> Pair (POS XH) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (NR ys)))
                           RRight ->
                             (case inside_square_2_dec_inf o1 o2 of
                                LLeft -> Pair (NEG XH) (Pair (Pair (Pair a
                                  (Pair b (Pair c d))) (Pair e (Pair f
                                  (Pair g h)))) (Pair (NR xs) (NR ys)))
                                RRight ->
                                  qquadratic_sign a (zplus a b)
                                    (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) e
                                    (zplus e f) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) xs ys))))
            DL ys ->
              (case three_integers_dec_inf b c d of
                 LLeft ->
                   (case three_integers_dec_inf f g h of
                      LLeft -> Pair (zmult (zsgn a) (zsgn e)) (Pair (Pair
                        (Pair a (Pair b (Pair c d))) (Pair e (Pair f
                        (Pair g h)))) (Pair (NR xs) (DL ys)))
                      RRight ->
                        (case z_lt_dec (POS (XO XH)) o2 of
                           LLeft -> Pair (zsgn a) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (DL ys)))
                           RRight ->
                             (case z_lt_dec o2 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn a)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (NR xs) (DL
                                  ys)))
                                RRight ->
                                  qquadratic_sign (zplus a b) b
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus e f) f
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) xs ys)))
                 RRight ->
                   (case three_integers_dec_inf f g h of
                      LLeft ->
                        (case z_lt_dec (POS (XO XH)) o1 of
                           LLeft -> Pair (zsgn e) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (DL ys)))
                           RRight ->
                             (case z_lt_dec o1 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn e)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (NR xs) (DL
                                  ys)))
                                RRight ->
                                  qquadratic_sign (zplus a b) b
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus e f) f
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) xs ys))
                      RRight ->
                        (case inside_square_1_dec_inf o1 o2 of
                           LLeft -> Pair (POS XH) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (NR xs) (DL ys)))
                           RRight ->
                             (case inside_square_2_dec_inf o1 o2 of
                                LLeft -> Pair (NEG XH) (Pair (Pair (Pair a
                                  (Pair b (Pair c d))) (Pair e (Pair f
                                  (Pair g h)))) (Pair (NR xs) (DL ys)))
                                RRight ->
                                  qquadratic_sign (zplus a b) b
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus e f) f
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) xs ys))))
            One ->
              let
                   l3 = qhomographic_sign (zplus a b) (zplus c d)
                          (zplus e f) (zplus g h) (NR xs)
              in
              let l2 = ffst (ssnd l3) in
              Pair (ffst l3) (Pair (Pair (Pair ZERO (Pair (ffst l2) (Pair
              ZERO (ffst (ssnd l2))))) (Pair ZERO (Pair
              (ffst (ssnd (ssnd l2))) (Pair ZERO (ssnd (ssnd (ssnd l2)))))))
              (Pair (ssnd (ssnd l3)) One)))
       DL xs ->
         (case p2 of
            NR ys ->
              (case three_integers_dec_inf b c d of
                 LLeft ->
                   (case three_integers_dec_inf f g h of
                      LLeft -> Pair (zmult (zsgn a) (zsgn e)) (Pair (Pair
                        (Pair a (Pair b (Pair c d))) (Pair e (Pair f
                        (Pair g h)))) (Pair (DL xs) (NR ys)))
                      RRight ->
                        (case z_lt_dec (POS (XO XH)) o2 of
                           LLeft -> Pair (zsgn a) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (NR ys)))
                           RRight ->
                             (case z_lt_dec o2 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn a)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (DL xs) (NR
                                  ys)))
                                RRight ->
                                  qquadratic_sign (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) c
                                    (zplus c d) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) g
                                    (zplus g h) xs ys)))
                 RRight ->
                   (case three_integers_dec_inf f g h of
                      LLeft ->
                        (case z_lt_dec (POS (XO XH)) o1 of
                           LLeft -> Pair (zsgn e) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (NR ys)))
                           RRight ->
                             (case z_lt_dec o1 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn e)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (DL xs) (NR
                                  ys)))
                                RRight ->
                                  qquadratic_sign (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) c
                                    (zplus c d) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) g
                                    (zplus g h) xs ys))
                      RRight ->
                        (case inside_square_1_dec_inf o1 o2 of
                           LLeft -> Pair (POS XH) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (NR ys)))
                           RRight ->
                             (case inside_square_2_dec_inf o1 o2 of
                                LLeft -> Pair (NEG XH) (Pair (Pair (Pair a
                                  (Pair b (Pair c d))) (Pair e (Pair f
                                  (Pair g h)))) (Pair (DL xs) (NR ys)))
                                RRight ->
                                  qquadratic_sign (zplus a c)
                                    (zplus (zplus (zplus a b) c) d) c
                                    (zplus c d) (zplus e g)
                                    (zplus (zplus (zplus e f) g) h) g
                                    (zplus g h) xs ys))))
            DL ys ->
              (case three_integers_dec_inf b c d of
                 LLeft ->
                   (case three_integers_dec_inf f g h of
                      LLeft -> Pair (zmult (zsgn a) (zsgn e)) (Pair (Pair
                        (Pair a (Pair b (Pair c d))) (Pair e (Pair f
                        (Pair g h)))) (Pair (DL xs) (DL ys)))
                      RRight ->
                        (case z_lt_dec (POS (XO XH)) o2 of
                           LLeft -> Pair (zsgn a) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (DL ys)))
                           RRight ->
                             (case z_lt_dec o2 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn a)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (DL xs) (DL
                                  ys)))
                                RRight ->
                                  qquadratic_sign
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus c d) d
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) (zplus g h) h xs ys)))
                 RRight ->
                   (case three_integers_dec_inf f g h of
                      LLeft ->
                        (case z_lt_dec (POS (XO XH)) o1 of
                           LLeft -> Pair (zsgn e) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (DL ys)))
                           RRight ->
                             (case z_lt_dec o1 (NEG (XO XH)) of
                                LLeft -> Pair (zopp (zsgn e)) (Pair (Pair
                                  (Pair a (Pair b (Pair c d))) (Pair e
                                  (Pair f (Pair g h)))) (Pair (DL xs) (DL
                                  ys)))
                                RRight ->
                                  qquadratic_sign
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus c d) d
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) (zplus g h) h xs ys))
                      RRight ->
                        (case inside_square_1_dec_inf o1 o2 of
                           LLeft -> Pair (POS XH) (Pair (Pair (Pair a
                             (Pair b (Pair c d))) (Pair e (Pair f (Pair g
                             h)))) (Pair (DL xs) (DL ys)))
                           RRight ->
                             (case inside_square_2_dec_inf o1 o2 of
                                LLeft -> Pair (NEG XH) (Pair (Pair (Pair a
                                  (Pair b (Pair c d))) (Pair e (Pair f
                                  (Pair g h)))) (Pair (DL xs) (DL ys)))
                                RRight ->
                                  qquadratic_sign
                                    (zplus (zplus (zplus a b) c) d)
                                    (zplus b d) (zplus c d) d
                                    (zplus (zplus (zplus e f) g) h)
                                    (zplus f h) (zplus g h) h xs ys))))
            One ->
              let
                   l3 = qhomographic_sign (zplus a b) (zplus c d)
                          (zplus e f) (zplus g h) (DL xs)
              in
              let l2 = ffst (ssnd l3) in
              Pair (ffst l3) (Pair (Pair (Pair ZERO (Pair (ffst l2) (Pair
              ZERO (ffst (ssnd l2))))) (Pair ZERO (Pair
              (ffst (ssnd (ssnd l2))) (Pair ZERO (ssnd (ssnd (ssnd l2)))))))
              (Pair (ssnd (ssnd l3)) One)))
       One ->
         let
              l3 = qhomographic_sign (zplus a c) (zplus b d) (zplus e g)
                     (zplus f h) p2
         in
         let l2 = ffst (ssnd l3) in
         Pair (ffst l3) (Pair (Pair (Pair ZERO (Pair ZERO (Pair (ffst l2)
         (ffst (ssnd l2))))) (Pair ZERO (Pair ZERO (Pair
         (ffst (ssnd (ssnd l2))) (ssnd (ssnd (ssnd l2))))))) (Pair One
         (ssnd (ssnd l3)))))
  
  qquadratic_sign_sign a b c d e f g h p1 p2 =
    case p1 of
      NR p ->
        (case p2 of
           NR p0 ->
             (case three_integers_dec_inf b c d of
                LLeft ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       eq_rec_r (Pair (zmult (zsgn a) (zsgn e)) (Pair
                         (Pair (Pair a (Pair b (Pair c d))) (Pair e (Pair
                         f (Pair g h)))) (Pair (NR p) (NR p0))))
                         (eq_rec (zsgn (zmult a e)) (zsgn_1 (zmult a e))
                           (zmult (zsgn a) (zsgn e)))
                         (qquadratic_sign a b c d e f g h (NR p) (NR p0))
                     RRight ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn a) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (NR p0)))) (zsgn_1 a)
                              (qquadratic_sign a b c d e f g h (NR p) (NR
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square e f g h) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn a)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (NR p) (NR p0))))
                                   (eq_rec (zsgn (zopp a))
                                     (zsgn_1 (zopp a)) (zopp (zsgn a)))
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0)))))
                RRight ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square a b c d) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn e) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (NR p0)))) (zsgn_1 e)
                              (qquadratic_sign a b c d e f g h (NR p) (NR
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square a b c d) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn e)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (NR p) (NR p0))))
                                   (eq_rec (zsgn (zopp e))
                                     (zsgn_1 (zopp e)) (zopp (zsgn e)))
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0))))
                     RRight ->
                       (case inside_square_1_dec_inf
                               (outside_square a b c d)
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (POS XH) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (NR p0)))) (Inleft
                              RRight)
                              (qquadratic_sign a b c d e f g h (NR p) (NR
                                p0))
                          RRight ->
                            (case inside_square_2_dec_inf
                                    (outside_square a b c d)
                                    (outside_square e f g h) of
                               LLeft ->
                                 eq_rec_r (Pair (NEG XH) (Pair (Pair
                                   (Pair a (Pair b (Pair c d))) (Pair e
                                   (Pair f (Pair g h)))) (Pair (NR p) (NR
                                   p0)))) Inright
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign_sign a (zplus a b)
                                     (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) e
                                     (zplus e f) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) p
                                     p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (NR p0))))))
           DL p0 ->
             (case three_integers_dec_inf b c d of
                LLeft ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       eq_rec_r (Pair (zmult (zsgn a) (zsgn e)) (Pair
                         (Pair (Pair a (Pair b (Pair c d))) (Pair e (Pair
                         f (Pair g h)))) (Pair (NR p) (DL p0))))
                         (eq_rec (zsgn (zmult a e)) (zsgn_1 (zmult a e))
                           (zmult (zsgn a) (zsgn e)))
                         (qquadratic_sign a b c d e f g h (NR p) (DL p0))
                     RRight ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn a) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (DL p0)))) (zsgn_1 a)
                              (qquadratic_sign a b c d e f g h (NR p) (DL
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square e f g h) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn a)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (NR p) (DL p0))))
                                   (eq_rec (zsgn (zopp a))
                                     (zsgn_1 (zopp a)) (zopp (zsgn a)))
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0)))))
                RRight ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square a b c d) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn e) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (DL p0)))) (zsgn_1 e)
                              (qquadratic_sign a b c d e f g h (NR p) (DL
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square a b c d) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn e)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (NR p) (DL p0))))
                                   (eq_rec (zsgn (zopp e))
                                     (zsgn_1 (zopp e)) (zopp (zsgn e)))
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0))))
                     RRight ->
                       (case inside_square_1_dec_inf
                               (outside_square a b c d)
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (POS XH) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (NR p) (DL p0)))) (Inleft
                              RRight)
                              (qquadratic_sign a b c d e f g h (NR p) (DL
                                p0))
                          RRight ->
                            (case inside_square_2_dec_inf
                                    (outside_square a b c d)
                                    (outside_square e f g h) of
                               LLeft ->
                                 eq_rec_r (Pair (NEG XH) (Pair (Pair
                                   (Pair a (Pair b (Pair c d))) (Pair e
                                   (Pair f (Pair g h)))) (Pair (NR p) (DL
                                   p0)))) Inright
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign_sign (zplus a b) b
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus e f) f
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) p p0)
                                   (qquadratic_sign a b c d e f g h (NR
                                     p) (DL p0))))))
           One ->
             let
                  l3 = qhomographic_sign (zplus a b) (zplus c d)
                         (zplus e f) (zplus g h) (NR p)
             in
             let l1' = ffst l3 in
             let l2 = ffst (ssnd l3) in
             eq_rec_r (Pair l1' (Pair (Pair (Pair ZERO (Pair (ffst l2)
               (Pair ZERO (ffst (ssnd l2))))) (Pair ZERO (Pair
               (ffst (ssnd (ssnd l2))) (Pair ZERO (ssnd (ssnd (ssnd l2)))))))
               (Pair (ssnd (ssnd l3)) One)))
               (eq_rec
                 (h_sign (zplus a b) (zplus c d) (zplus e f) (zplus g h)
                   (NR p))
                 (sg_sign_dec (zplus a b) (zplus c d) (zplus e f)
                   (zplus g h) (NR p)) l1')
               (qquadratic_sign a b c d e f g h (NR p) One))
      DL p ->
        (case p2 of
           NR p0 ->
             (case three_integers_dec_inf b c d of
                LLeft ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       eq_rec_r (Pair (zmult (zsgn a) (zsgn e)) (Pair
                         (Pair (Pair a (Pair b (Pair c d))) (Pair e (Pair
                         f (Pair g h)))) (Pair (DL p) (NR p0))))
                         (eq_rec (zsgn (zmult a e)) (zsgn_1 (zmult a e))
                           (zmult (zsgn a) (zsgn e)))
                         (qquadratic_sign a b c d e f g h (DL p) (NR p0))
                     RRight ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn a) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (NR p0)))) (zsgn_1 a)
                              (qquadratic_sign a b c d e f g h (DL p) (NR
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square e f g h) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn a)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (DL p) (NR p0))))
                                   (eq_rec (zsgn (zopp a))
                                     (zsgn_1 (zopp a)) (zopp (zsgn a)))
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0)))))
                RRight ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square a b c d) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn e) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (NR p0)))) (zsgn_1 e)
                              (qquadratic_sign a b c d e f g h (DL p) (NR
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square a b c d) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn e)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (DL p) (NR p0))))
                                   (eq_rec (zsgn (zopp e))
                                     (zsgn_1 (zopp e)) (zopp (zsgn e)))
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0))))
                     RRight ->
                       (case inside_square_1_dec_inf
                               (outside_square a b c d)
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (POS XH) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (NR p0)))) (Inleft
                              RRight)
                              (qquadratic_sign a b c d e f g h (DL p) (NR
                                p0))
                          RRight ->
                            (case inside_square_2_dec_inf
                                    (outside_square a b c d)
                                    (outside_square e f g h) of
                               LLeft ->
                                 eq_rec_r (Pair (NEG XH) (Pair (Pair
                                   (Pair a (Pair b (Pair c d))) (Pair e
                                   (Pair f (Pair g h)))) (Pair (DL p) (NR
                                   p0)))) Inright
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign_sign (zplus a c)
                                     (zplus (zplus (zplus a b) c) d) c
                                     (zplus c d) (zplus e g)
                                     (zplus (zplus (zplus e f) g) h) g
                                     (zplus g h) p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (NR p0))))))
           DL p0 ->
             (case three_integers_dec_inf b c d of
                LLeft ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       eq_rec_r (Pair (zmult (zsgn a) (zsgn e)) (Pair
                         (Pair (Pair a (Pair b (Pair c d))) (Pair e (Pair
                         f (Pair g h)))) (Pair (DL p) (DL p0))))
                         (eq_rec (zsgn (zmult a e)) (zsgn_1 (zmult a e))
                           (zmult (zsgn a) (zsgn e)))
                         (qquadratic_sign a b c d e f g h (DL p) (DL p0))
                     RRight ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn a) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (DL p0)))) (zsgn_1 a)
                              (qquadratic_sign a b c d e f g h (DL p) (DL
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square e f g h) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn a)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (DL p) (DL p0))))
                                   (eq_rec (zsgn (zopp a))
                                     (zsgn_1 (zopp a)) (zopp (zsgn a)))
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0)))))
                RRight ->
                  (case three_integers_dec_inf f g h of
                     LLeft ->
                       (case z_lt_dec (POS (XO XH))
                               (outside_square a b c d) of
                          LLeft ->
                            eq_rec_r (Pair (zsgn e) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (DL p0)))) (zsgn_1 e)
                              (qquadratic_sign a b c d e f g h (DL p) (DL
                                p0))
                          RRight ->
                            (case z_lt_dec (outside_square a b c d) (NEG
                                    (XO XH)) of
                               LLeft ->
                                 eq_rec_r (Pair (zopp (zsgn e)) (Pair
                                   (Pair (Pair a (Pair b (Pair c d)))
                                   (Pair e (Pair f (Pair g h)))) (Pair
                                   (DL p) (DL p0))))
                                   (eq_rec (zsgn (zopp e))
                                     (zsgn_1 (zopp e)) (zopp (zsgn e)))
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0))))
                     RRight ->
                       (case inside_square_1_dec_inf
                               (outside_square a b c d)
                               (outside_square e f g h) of
                          LLeft ->
                            eq_rec_r (Pair (POS XH) (Pair (Pair (Pair a
                              (Pair b (Pair c d))) (Pair e (Pair f (Pair
                              g h)))) (Pair (DL p) (DL p0)))) (Inleft
                              RRight)
                              (qquadratic_sign a b c d e f g h (DL p) (DL
                                p0))
                          RRight ->
                            (case inside_square_2_dec_inf
                                    (outside_square a b c d)
                                    (outside_square e f g h) of
                               LLeft ->
                                 eq_rec_r (Pair (NEG XH) (Pair (Pair
                                   (Pair a (Pair b (Pair c d))) (Pair e
                                   (Pair f (Pair g h)))) (Pair (DL p) (DL
                                   p0)))) Inright
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0))
                               RRight ->
                                 eq_rec_r
                                   (qquadratic_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign_sign
                                     (zplus (zplus (zplus a b) c) d)
                                     (zplus b d) (zplus c d) d
                                     (zplus (zplus (zplus e f) g) h)
                                     (zplus f h) (zplus g h) h p p0)
                                   (qquadratic_sign a b c d e f g h (DL
                                     p) (DL p0))))))
           One ->
             let
                  l3 = qhomographic_sign (zplus a b) (zplus c d)
                         (zplus e f) (zplus g h) (DL p)
             in
             let l1' = ffst l3 in
             let l2 = ffst (ssnd l3) in
             eq_rec_r (Pair l1' (Pair (Pair (Pair ZERO (Pair (ffst l2)
               (Pair ZERO (ffst (ssnd l2))))) (Pair ZERO (Pair
               (ffst (ssnd (ssnd l2))) (Pair ZERO (ssnd (ssnd (ssnd l2)))))))
               (Pair (ssnd (ssnd l3)) One)))
               (eq_rec
                 (h_sign (zplus a b) (zplus c d) (zplus e f) (zplus g h)
                   (DL p))
                 (sg_sign_dec (zplus a b) (zplus c d) (zplus e f)
                   (zplus g h) (DL p)) l1')
               (qquadratic_sign a b c d e f g h (DL p) One))
      One ->
        let
             l3 = qhomographic_sign (zplus a c) (zplus b d) (zplus e g)
                    (zplus f h) p2
        in
        let l1' = ffst l3 in
        let l2 = ffst (ssnd l3) in
        eq_rec_r (Pair l1' (Pair (Pair (Pair ZERO (Pair ZERO (Pair
          (ffst l2) (ffst (ssnd l2))))) (Pair ZERO (Pair ZERO (Pair
          (ffst (ssnd (ssnd l2))) (ssnd (ssnd (ssnd l2))))))) (Pair One
          (ssnd (ssnd l3)))))
          (eq_rec
            (h_sign (zplus a c) (zplus b d) (zplus e g) (zplus f h) p2)
            (sg_sign_dec (zplus a c) (zplus b d) (zplus e g) (zplus f h)
              p2) l1') (qquadratic_sign a b c d e f g h One p2)
  
  qquadratic_sign_sign_dec a b c d e f g h p1 p2 =
    qquadratic_sign_sign a b c d e f g h p1 p2
  
  octo_leq_inf a b c d e f g h =
    case z_le_dec e a of
      LLeft ->
        (case z_le_dec f b of
           LLeft ->
             (case z_le_dec g c of
                LLeft -> z_le_dec h d
                RRight -> RRight)
           RRight -> RRight)
      RRight -> RRight
  
  quadratic_top_more_informative a b c d e f g h =
    case octo_leq_inf a b c d e f g h of
      LLeft ->
        (case z_le_lt_eq_dec e a of
           LLeft -> LLeft
           RRight ->
             (case z_le_lt_eq_dec f b of
                LLeft -> LLeft
                RRight ->
                  (case z_le_lt_eq_dec g c of
                     LLeft -> LLeft
                     RRight -> z_le_lt_eq_dec h d)))
      RRight -> RRight
  
  qquadratic_Qpositive_to_Qpositive a b c d e f g h p1 p2 =
    case qpositive_dec_One p1 of
      LLeft ->
        qhomographic_Qpositive_to_Qpositive (zplus a c) (zplus b d)
          (zplus e g) (zplus f h) p2
      RRight ->
        (case qpositive_dec_One p2 of
           LLeft ->
             qhomographic_Qpositive_to_Qpositive (zplus a b) (zplus c d)
               (zplus e f) (zplus g h) p1
           RRight ->
             (case quadratic_top_more_informative a b c d e f g h of
                LLeft -> NR
                  (qquadratic_Qpositive_to_Qpositive (zminus a e)
                    (zminus b f) (zminus c g) (zminus d h) e f g h p1 p2)
                RRight ->
                  (case quadratic_top_more_informative e f g h a b c d of
                     LLeft -> DL
                       (qquadratic_Qpositive_to_Qpositive a b c d
                         (zminus e a) (zminus f b) (zminus g c)
                         (zminus h d) p1 p2)
                     RRight ->
                       (case p1 of
                          NR x ->
                            (case p2 of
                               NR ys ->
                                 qquadratic_Qpositive_to_Qpositive a
                                   (zplus a b) (zplus a c)
                                   (zplus (zplus (zplus a b) c) d) e
                                   (zplus e f) (zplus e g)
                                   (zplus (zplus (zplus e f) g) h) x ys
                               DL ys ->
                                 qquadratic_Qpositive_to_Qpositive
                                   (zplus a b) b
                                   (zplus (zplus (zplus a b) c) d)
                                   (zplus b d) (zplus e f) f
                                   (zplus (zplus (zplus e f) g) h)
                                   (zplus f h) x ys
                               One -> false_rec __ x __)
                          DL x ->
                            (case p2 of
                               NR ys ->
                                 qquadratic_Qpositive_to_Qpositive
                                   (zplus a c)
                                   (zplus (zplus (zplus a b) c) d) c
                                   (zplus c d) (zplus e g)
                                   (zplus (zplus (zplus e f) g) h) g
                                   (zplus g h) x ys
                               DL ys ->
                                 qquadratic_Qpositive_to_Qpositive
                                   (zplus (zplus (zplus a b) c) d)
                                   (zplus b d) (zplus c d) d
                                   (zplus (zplus (zplus e f) g) h)
                                   (zplus f h) (zplus g h) h x ys
                               One -> false_rec __ x __)
                          One -> false_rec __))))
  
  same_ratio_dec_inf a b c d e f g h =
    case z_eq_dec (zmult a f) (zmult b e) of
      LLeft ->
        (case z_eq_dec (zmult b g) (zmult c f) of
           LLeft ->
             (case z_eq_dec (zmult c h) (zmult d g) of
                LLeft ->
                  (case z_eq_dec (zmult a g) (zmult c e) of
                     LLeft ->
                       (case z_eq_dec (zmult a h) (zmult d e) of
                          LLeft -> z_eq_dec (zmult b h) (zmult d f)
                          RRight -> RRight)
                     RRight -> RRight)
                RRight -> RRight)
           RRight -> RRight)
      RRight -> RRight
  
  qnew_a a b c d e f g h p1 p2 =
    ffst (ffst (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))
  
  qnew_b a b c d e f g h p1 p2 =
    ffst (ssnd (ffst (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2)))))
  
  qnew_c a b c d e f g h p1 p2 =
    ffst
      (ssnd
        (ssnd (ffst (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))))
  
  qnew_d a b c d e f g h p1 p2 =
    ssnd
      (ssnd
        (ssnd (ffst (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))))
  
  qnew_e a b c d e f g h p1 p2 =
    ffst (ssnd (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))
  
  qnew_f a b c d e f g h p1 p2 =
    ffst (ssnd (ssnd (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2)))))
  
  qnew_g a b c d e f g h p1 p2 =
    ffst
      (ssnd
        (ssnd (ssnd (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))))
  
  qnew_h a b c d e f g h p1 p2 =
    ssnd
      (ssnd
        (ssnd (ssnd (ffst (ssnd (qquadratic_sign a b c d e f g h p1 p2))))))
  
  qnew_p1 a b c d e f g h p1 p2 =
    ffst (ssnd (ssnd (qquadratic_sign a b c d e f g h p1 p2)))
  
  qnew_p2 a b c d e f g h p1 p2 =
    ssnd (ssnd (ssnd (qquadratic_sign a b c d e f g h p1 p2)))
  
  qquadratic_sg_denom_nonzero_nonzero_inf e f g h p1 p2 =
    case z_zerop e of
      LLeft ->
        (case z_zerop f of
           LLeft ->
             (case z_zerop g of
                LLeft ->
                  (case z_zerop h of
                     LLeft -> false_rec __
                     RRight -> Inright)
                RRight -> Inleft Inright)
           RRight -> Inleft (Inleft RRight))
      RRight -> Inleft (Inleft LLeft)
  
  qquadratic_Qpositive_to_Q_subproof0 a b c d e f g h p1 p2 =
    false_rec __
  
  qquadratic_Qpositive_to_Q_subproof4 a b c d e f g h p1 p2 =
    false_rec __
  
  qquadratic_Qpositive_to_Q a b c d e f g h p1 p2 =
    case same_ratio_dec_inf a b c d e f g h of
      LLeft ->
        (case qquadratic_sg_denom_nonzero_nonzero_inf e f g h p1 p2 of
           Inleft s ->
             (case s of
                Inleft s0 ->
                  (case s0 of
                     LLeft -> fraction_encoding a e
                     RRight -> fraction_encoding b f)
                Inright -> fraction_encoding c g)
           Inright -> fraction_encoding d h)
      RRight ->
        (case qquadratic_sign_sign_dec a b c d e f g h p1 p2 of
           Inleft s ->
             (case s of
                LLeft -> Zero
                RRight ->
                  (case zsgn_1
                          (zplus
                            (zplus
                              (zplus (qnew_a a b c d e f g h p1 p2)
                                (qnew_b a b c d e f g h p1 p2))
                              (qnew_c a b c d e f g h p1 p2))
                            (qnew_d a b c d e f g h p1 p2)) of
                     Inleft s0 ->
                       (case s0 of
                          LLeft ->
                            qquadratic_Qpositive_to_Q_subproof0 a b c d e
                              f g h p1 p2
                          RRight -> Qpos
                            (qquadratic_Qpositive_to_Qpositive
                              (qnew_a a b c d e f g h p1 p2)
                              (qnew_b a b c d e f g h p1 p2)
                              (qnew_c a b c d e f g h p1 p2)
                              (qnew_d a b c d e f g h p1 p2)
                              (qnew_e a b c d e f g h p1 p2)
                              (qnew_f a b c d e f g h p1 p2)
                              (qnew_g a b c d e f g h p1 p2)
                              (qnew_h a b c d e f g h p1 p2)
                              (qnew_p1 a b c d e f g h p1 p2)
                              (qnew_p2 a b c d e f g h p1 p2)))
                     Inright -> Qpos
                       (qquadratic_Qpositive_to_Qpositive
                         (zopp (qnew_a a b c d e f g h p1 p2))
                         (zopp (qnew_b a b c d e f g h p1 p2))
                         (zopp (qnew_c a b c d e f g h p1 p2))
                         (zopp (qnew_d a b c d e f g h p1 p2))
                         (zopp (qnew_e a b c d e f g h p1 p2))
                         (zopp (qnew_f a b c d e f g h p1 p2))
                         (zopp (qnew_g a b c d e f g h p1 p2))
                         (zopp (qnew_h a b c d e f g h p1 p2))
                         (qnew_p1 a b c d e f g h p1 p2)
                         (qnew_p2 a b c d e f g h p1 p2))))
           Inright ->
             (case zsgn_1
                     (zplus
                       (zplus
                         (zplus (qnew_a a b c d e f g h p1 p2)
                           (qnew_b a b c d e f g h p1 p2))
                         (qnew_c a b c d e f g h p1 p2))
                       (qnew_d a b c d e f g h p1 p2)) of
                Inleft s ->
                  (case s of
                     LLeft ->
                       qquadratic_Qpositive_to_Q_subproof4 a b c d e f g
                         h p1 p2
                     RRight -> Qneg
                       (qquadratic_Qpositive_to_Qpositive
                         (qnew_a a b c d e f g h p1 p2)
                         (qnew_b a b c d e f g h p1 p2)
                         (qnew_c a b c d e f g h p1 p2)
                         (qnew_d a b c d e f g h p1 p2)
                         (zopp (qnew_e a b c d e f g h p1 p2))
                         (zopp (qnew_f a b c d e f g h p1 p2))
                         (zopp (qnew_g a b c d e f g h p1 p2))
                         (zopp (qnew_h a b c d e f g h p1 p2))
                         (qnew_p1 a b c d e f g h p1 p2)
                         (qnew_p2 a b c d e f g h p1 p2)))
                Inright -> Qneg
                  (qquadratic_Qpositive_to_Qpositive
                    (zopp (qnew_a a b c d e f g h p1 p2))
                    (zopp (qnew_b a b c d e f g h p1 p2))
                    (zopp (qnew_c a b c d e f g h p1 p2))
                    (zopp (qnew_d a b c d e f g h p1 p2))
                    (qnew_e a b c d e f g h p1 p2)
                    (qnew_f a b c d e f g h p1 p2)
                    (qnew_g a b c d e f g h p1 p2)
                    (qnew_h a b c d e f g h p1 p2)
                    (qnew_p1 a b c d e f g h p1 p2)
                    (qnew_p2 a b c d e f g h p1 p2))))
  
  qquadratic a b c d e f g h s1 s2 =
    case s1 of
      Zero -> qhomographic c d g h s2
      Qpos p1 ->
        (case s2 of
           Zero -> qhomographic b d f h (Qpos p1)
           Qpos p2 -> qquadratic_Qpositive_to_Q a b c d e f g h p1 p2
           Qneg p2 ->
             qquadratic_Qpositive_to_Q (zopp a) b (zopp c) d (zopp e) f
               (zopp g) h p1 p2)
      Qneg p1 ->
        (case s2 of
           Zero -> qhomographic b d f h (Qneg p1)
           Qpos p2 ->
             qquadratic_Qpositive_to_Q (zopp a) (zopp b) c d (zopp e)
               (zopp f) g h p1 p2
           Qneg p2 ->
             qquadratic_Qpositive_to_Q a (zopp b) (zopp c) d e (zopp f)
               (zopp g) h p1 p2)
  
  
  
  -- Upto here was generated using ^Coq> Extraction "quadratic" Qquadratic^ in Coq 
  -- Now we add pretty printing facilities 
  
  showQPos One = ""
  showQPos (DL p') = 'L': (showQPos p')
  showQPos (NR p') = 'R': (showQPos p')
  
  
  showQ Zero = "0"
  showQ (Qpos p') = (showQPos p')
  showQ (Qneg p') =  '-':(showQPos p')
  
  
  nattoPos x = if x==1 then XH 
               else if (mod x 2)==1 then (XI (nattoPos (div x 2)))
                    else (XO (nattoPos (div x 2)))
  
  toZ x = if x==0 then ZERO
                     else if (x>0) then (POS (nattoPos x))
                                   else (NEG (nattoPos (-x)))
  
  toQPos "I"= One
  toQPos "" = One
  toQPos ('L':xs) = (DL (toQPos xs))
  toQPos ('R':xs) = (NR (toQPos xs))
  
  toQ "0"= Zero
  toQ ('-':xs) = (Qneg (toQPos xs))
  toQ ('+':xs) = (Qpos (toQPos xs))
  toQ (x:xs) = (Qpos (toQPos (x:xs)))
  
  fraction_encoding_ x y= showQ (fraction_encoding (toZ x) (toZ y))
  
  qhomographic_Qpositive_to_Qpositive_ a b c d p= showQPos (qhomographic_Qpositive_to_Qpositive (toZ a) (toZ b) (toZ c) (toZ d) (toQPos p)) 
  
  qhomographic_ a b c d x = showQ (qhomographic (toZ a) (toZ b) (toZ c) (toZ d) (toQ x))
  
  qquadratic_Qpositive_to_Qpositive_ a b c d e f g h p1 p2 = showQPos (qquadratic_Qpositive_to_Qpositive (toZ a) (toZ b) (toZ c) (toZ d) (toZ e) (toZ f) (toZ g) (toZ h) (toQPos p1) (toQPos p2)) 
  
  qquadratic_ a b c d e f g h x y = showQ  (qquadratic (toZ a) (toZ b) (toZ c) (toZ d) (toZ e) (toZ f) (toZ g) (toZ h) (toQ x) (toQ y)) 
  
  lazy_plus_ x y = qquadratic_  0 1 1 0 0 0 0 1 x y
  
  lazy_mult_ x y = qquadratic_  1 0 0 0 0 0 0 1 x y
  
  lazy_minus_ x y = qquadratic_  0 1 (-1) 0 0 0 0 1 x y 
  
  lazy_div_ x y = qquadratic_  0 1 0 0 0 0 1 0 x y
  