Theory hrat

⊢ hrat_1 = hrat_ABS trat_1

⊢ ∀r. hrat_ABS r = hrat_ABS_CLASS ($trat_eq r)

⊢ ∀a. hrat_REP a = $@ (hrat_REP_CLASS a)

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. r trat_eq r ∧ (c = $trat_eq r)) rep

⊢ ∀T1 T2. T1 hrat_add T2 = hrat_ABS (hrat_REP T1 trat_add hrat_REP T2)

⊢ (∀a. hrat_ABS_CLASS (hrat_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. r trat_eq r ∧ (c = $trat_eq r)) r ⇔
      (hrat_REP_CLASS (hrat_ABS_CLASS r) = r)

⊢ ∀T1. hrat_inv T1 = hrat_ABS (trat_inv (hrat_REP T1))

⊢ ∀T1 T2. T1 hrat_mul T2 = hrat_ABS (hrat_REP T1 trat_mul hrat_REP T2)

⊢ ∀T1. hrat_sucint T1 = hrat_ABS (trat_sucint T1)

⊢ trat_1 = (0,0)

⊢ ∀x y x' y'.
    (x,y) trat_add (x',y') =
    (PRE (SUC x * SUC y' + SUC x' * SUC y),PRE (SUC y * SUC y'))

⊢ ∀x y x' y'. (x,y) trat_eq (x',y') ⇔ (SUC x * SUC y' = SUC x' * SUC y)

⊢ ∀x y. trat_inv (x,y) = (y,x)

⊢ ∀x y x' y'.
    (x,y) trat_mul (x',y') = (PRE (SUC x * SUC x'),PRE (SUC y * SUC y'))

⊢ (trat_sucint 0 = trat_1) ∧
  ∀n. trat_sucint (SUC n) = trat_sucint n trat_add trat_1

⊢ ∀h i j. h hrat_add (i hrat_add j) = h hrat_add i hrat_add j

⊢ ∀h i. h hrat_add i = i hrat_add h

⊢ ∀h i. (h = i) ∨ (∃d. h = i hrat_add d) ∨ ∃d. i = h hrat_add d

⊢ ∀h. ∃n d. hrat_sucint n = h hrat_add d

⊢ ∀h i j. h hrat_mul (i hrat_add j) = h hrat_mul i hrat_add h hrat_mul j

⊢ ∀h i j. h hrat_mul (i hrat_mul j) = h hrat_mul i hrat_mul j

⊢ ∀h. hrat_1 hrat_mul h = h

⊢ ∀h. hrat_inv h hrat_mul h = hrat_1

⊢ ∀h i. h hrat_mul i = i hrat_mul h

⊢ ∀h i. h hrat_add i ≠ h

⊢ (hrat_sucint 0 = hrat_1) ∧
  ∀n. hrat_sucint (SUC n) = hrat_sucint n hrat_add hrat_1

⊢ ∀h i j. h trat_add (i trat_add j) trat_eq h trat_add i trat_add j

⊢ ∀h i. h trat_add i trat_eq i trat_add h

⊢ ∀h i. h trat_add i = i trat_add h

⊢ ∀h i.
    h trat_eq i ∨ (∃d. h trat_eq i trat_add d) ∨ ∃d. i trat_eq h trat_add d

⊢ ∀p q r. p trat_eq q ⇒ p trat_add r trat_eq q trat_add r

⊢ ∀p1 p2 q1 q2.
    p1 trat_eq p2 ∧ q1 trat_eq q2 ⇒ p1 trat_add q1 trat_eq p2 trat_add q2

⊢ ∀h. ∃n d. trat_sucint n trat_eq h trat_add d

⊢ ∀p q. (p = q) ⇒ p trat_eq q

⊢ ∀p q. p trat_eq q ⇔ ($trat_eq p = $trat_eq q)

⊢ ∀p. p trat_eq p

⊢ ∀p q. p trat_eq q ⇔ q trat_eq p

⊢ ∀p q r. p trat_eq q ∧ q trat_eq r ⇒ p trat_eq r

⊢ ∀p q. p trat_eq q ⇒ trat_inv p trat_eq trat_inv q

⊢ ∀h i j.
    h trat_mul (i trat_add j) trat_eq h trat_mul i trat_add h trat_mul j

⊢ ∀h i j. h trat_mul (i trat_mul j) trat_eq h trat_mul i trat_mul j

⊢ ∀h. trat_1 trat_mul h trat_eq h

⊢ ∀h. trat_inv h trat_mul h trat_eq trat_1

⊢ ∀h i. h trat_mul i trat_eq i trat_mul h

⊢ ∀h i. h trat_mul i = i trat_mul h

⊢ ∀p q r. p trat_eq q ⇒ p trat_mul r trat_eq q trat_mul r

⊢ ∀p1 p2 q1 q2.
    p1 trat_eq p2 ∧ q1 trat_eq q2 ⇒ p1 trat_mul q1 trat_eq p2 trat_mul q2

⊢ ∀h i. ¬(h trat_add i trat_eq h)

⊢ trat_sucint 0 trat_eq trat_1 ∧
  ∀n. trat_sucint (SUC n) trat_eq trat_sucint n trat_add trat_1

⊢ ∀n. trat_sucint n trat_eq (n,0)

⊢ (∀a. hrat_ABS_CLASS (hrat_REP_CLASS a) = a) ∧
  ∀c. (∃r. r trat_eq r ∧ (c = $trat_eq r)) ⇔
      (hrat_REP_CLASS (hrat_ABS_CLASS c) = c)

⊢ QUOTIENT $trat_eq hrat_ABS hrat_REP