Theory rat

⊢ ∀r. r = rat_of_int (RATN r) / &RATD r ∧ 0 < RATD r ∧
      (RATN r = 0 ⇒ RATD r = 1) ∧
      ∀n' d'. r = rat_of_int n' / &d' ∧ 0 < d' ⇒ ABS (RATN r) ≤ ABS n'

⊢ ∀r. abs_rat r = abs_rat_CLASS (rat_equiv r)

⊢ ∀a b.
    div_gcd a b =
    (let
       d = gcd (Num a) b
     in
       if d = 0 ∨ d = 1 then (a,b) else (a / &d,b DIV d))

⊢ rat_0 = abs_rat frac_0

⊢ rat_1 = abs_rat frac_1

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

⊢ ∀r1 r2. r1 + r2 = abs_rat (frac_add (rep_rat r1) (rep_rat r2))

⊢ ∀r1. -r1 = abs_rat (frac_ainv (rep_rat r1))

⊢ (∀a. abs_rat_CLASS (rep_rat_CLASS a) = a) ∧
  ∀r. (λc. ∃r. rat_equiv r r ∧ c = rat_equiv r) r ⇔
      rep_rat_CLASS (abs_rat_CLASS r) = r

⊢ ∀nmr dnm.
    nmr // dnm = abs_rat (abs_frac (SGN nmr * SGN dnm * ABS nmr,ABS dnm))

⊢ ∀r1 r2. r1 / r2 = abs_rat (frac_div (rep_rat r1) (rep_rat r2))

⊢ ∀r. rat_dnm r = frac_dnm (rep_rat r)

⊢ ∀f1 f2.
    rat_equiv f1 f2 ⇔ frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

⊢ ∀r i.
    r ** i = if 0 ≤ i then expn r (Num i) else rat_minv (expn r (Num i))

⊢ (∀r. expn r 0 = 1) ∧ ∀r n. expn r (SUC n) = r * expn r n

⊢ ∀r1 r2. r1 ≥ r2 ⇔ r2 ≤ r1

⊢ ∀r1 r2. r1 > r2 ⇔ r2 < r1

⊢ ∀r1 r2. r1 ≤ r2 ⇔ r1 < r2 ∨ r1 = r2

⊢ ∀r1 r2. r1 < r2 ⇔ RAT_SGN (r2 − r1) = 1

⊢ ∀r1 r2. rat_max r1 r2 = if r1 > r2 then r1 else r2

⊢ ∀r1 r2. rat_min r1 r2 = if r1 < r2 then r1 else r2

⊢ ∀r1. rat_minv r1 = abs_rat (frac_minv (rep_rat r1))

⊢ ∀r1 r2. r1 * r2 = abs_rat (frac_mul (rep_rat r1) (rep_rat r2))

⊢ ∀r. rat_nmr r = frac_nmr (rep_rat r)

⊢ ∀i. rat_of_int i = if i < 0 then -&Num (-i) else &Num i

⊢ $& =
  WFREC (@R. WF R ∧ ∀n. R (SUC n) (SUC (SUC n)))
    (λrat_of_num a.
         case a of
           0 => I rat_0
         | SUC 0 => I rat_1
         | SUC (SUC n) => I (rat_of_num (SUC n) + rat_1))

⊢ ∀r. RAT_SGN r = frac_sgn (rep_rat r)

⊢ ∀r1 r2. r1 − r2 = abs_rat (frac_sub (rep_rat r1) (rep_rat r2))

⊢ ∀a. rep_rat a = $@ (rep_rat_CLASS a)

⊢ 0 < d ⇒ abs_rat (abs_frac (n,d)) = rat_of_int n / rat_of_int d

⊢ abs_rat (abs_frac (RATN q,&RATD q)) = q

⊢ rat_equiv x x' ⇒ rat_equiv (frac_add x y) (frac_add x' y)

⊢ frac_nmr y ≠ 0 ⇒ rat_equiv x y ⇒ rat_equiv (frac_minv x) (frac_minv y)

⊢ rat_equiv x x' ⇒ rat_equiv (frac_mul x y) (frac_mul x' y)

⊢ rat_equiv x x' ⇒ rat_equiv (frac_mul y x) (frac_mul y x')

⊢ m ≠ 0 ⇒ (a * b) % m = (a % m * b % m) % m

⊢ r1 / r2 * r3 = r1 * r3 / r2

⊢ a < b ∧ (c < d ∨ c ≤ d ∧ d ≠ 0) ⇒ a * c < b * d

⊢ i ≠ 0 ⇒ Num i ≠ 0 ∧ 0 < Num i

⊢ 0 < i ⇒ ∃n. i = &SUC n

⊢ ∀r. abs_rat (rep_rat r) = r

⊢ RATD (-r) = RATD r

⊢ 0 < RATD r ∧ RATD r ≠ 0

⊢ RATN (&n) = &n ∧ RATD (&n) = 1

⊢ ∀p q. coprime p q ∧ q ≠ 0 ⇒ RATN (&p / &q) = &p ∧ RATD (&p / &q) = q

⊢ ∀p q. coprime p q ∧ q ≠ 0 ⇒ RATN (-&p / &q) = -&p ∧ RATD (-&p / &q) = q

⊢ coprime (Num n) d ∧ d ≠ 0 ⇒
  RATN (rat_of_int n / &d) = n ∧ RATD (rat_of_int n / &d) = d

⊢ rat_of_int (RATN r) / &RATD r = r

⊢ (RATN r = 0 ⇔ r = 0) ∧ (0 = RATN r ⇔ r = 0)

⊢ ∀n' d'. r = rat_of_int n' / &d' ∧ 0 < d' ⇒ ABS (RATN r) ≤ ABS n'

⊢ RATN (-r) = -RATN r

⊢ r = rat_of_int (RATN r) / &RATD r

⊢ r * &RATD r = rat_of_int (RATN r)

⊢ RATN (rat_of_int i) = i ∧ RATD (rat_of_int i) = 1

⊢ (0 < RATN x ⇔ 0 < x) ∧ (0 ≤ RATN x ⇔ 0 ≤ x) ∧ (RATN x < 0 ⇔ x < 0) ∧
  (RATN x ≤ 0 ⇔ x ≤ 0)

⊢ rat_0 = 0

⊢ ∀r1. 0 ≤ r1 ⇔ 0 ≤ rat_nmr r1

⊢ ∀r1 r2. 0 < r1 ⇒ 0 ≤ r2 ⇒ 0 < r1 + r2

⊢ ∀r1 r2. 0 < r1 ⇒ 0 < r2 ⇒ 0 < r1 + r2

⊢ ∀r1. 0 < r1 ⇔ 0 < rat_nmr r1

⊢ rat_1 = 1

⊢ 1 ≠ 0

⊢ ∀f1 f2. abs_rat f1 = abs_rat f2 ⇔ rat_equiv f1 f2

⊢ ∀a b c. a + (b + c) = a + b + c

⊢ ∀f1 f2. abs_rat f1 + abs_rat f2 = abs_rat (frac_add f1 f2)

⊢ ∀a b. a + b = b + a

⊢ (∀x y.
     abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)) ∧
  ∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)

⊢ ∀x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)

⊢ ∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)

⊢ ∀a. 0 + a = a

⊢ ∀a. -a + a = 0

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a + c ≤ b + d

⊢ (∀n m. &n + &m = &(n + m)) ∧
  (∀n m. -&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
  (∀n m. &n + -&m = if m ≤ n then &(n − m) else -&(m − n)) ∧
  ∀n m. -&n + -&m = -&(n + m)

⊢ ∀r1. ONE_ONE ($+ r1)

⊢ ∀a. a + 0 = a

⊢ ∀a. a + -a = 0

⊢ -0 = 0

⊢ ∀r1 r2. -(r1 + r2) = -r1 + -r2

⊢ ∀r1. --r1 = r1

⊢ ∀f1. -abs_rat f1 = abs_rat (frac_ainv f1)

⊢ ∀x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)

⊢ ∀r1 r2. -r1 = r2 ⇔ r1 = -r2

⊢ -x = &n ⇔ x = rat_of_int (-&n)

⊢ ∀r1 r2. -r1 < r2 ⇔ -r2 < r1

⊢ ∀r1 r2. -(r1 * r2) = -r1 * r2

⊢ ∀r1. r1 ≠ 0 ⇒ -rat_minv r1 = rat_minv (-r1)

⊢ -1 * r = -r

⊢ ONE_ONE numeric_negate

⊢ ∀r1 r2. -(r1 * r2) = r1 * -r2

⊢ (0 < -r ⇔ r < 0) ∧ (-r < 0 ⇔ 0 < r)

⊢ ∀r1 r2. -(r1 − r2) = r2 − r1

⊢ ∀n. &n // 1 = &n ∧ -&n // 1 = -&n

⊢ ∀r1 r3. r1 < r3 ⇒ ∃r2. r1 < r2 ∧ r2 < r3

⊢ y ≠ 0 ∧ b ≠ 0 ⇒ x / y + a / b = (x * b + a * y) / (y * b)

⊢ b ≠ 0 ∧ d ≠ 0 ⇒ a / b * (c / d) = a * c / (b * d)

⊢ d ≠ 0 ⇒ n / d * d = n

⊢ 0 / x = 0

⊢ r / 1 = r

⊢ -(x / y) = -x / y

⊢ ∀f1 f2.
    frac_nmr f2 ≠ 0 ⇒ abs_rat f1 / abs_rat f2 = abs_rat (frac_div f1 f2)

⊢ (∀x y.
     frac_nmr y ≠ 0 ⇒
     abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)) ∧
  ∀x y.
    frac_nmr y ≠ 0 ⇒
    abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)

⊢ ∀x y.
    frac_nmr y ≠ 0 ⇒
    abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)

⊢ ∀x y.
    frac_nmr y ≠ 0 ⇒
    abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)

⊢ d ≠ 0 ⇒ (n / d = 0 ⇔ n = 0) ∧ (0 = n / d ⇔ n = 0)

⊢ r ≠ 0 ⇒ r / r = 1

⊢ x ≠ 0 ∧ y ≠ 0 ⇒ rat_minv (x / y) = y / x

⊢ ∀r1 r2. r1 / r2 = r1 * rat_minv r2

⊢ r / -1 = -r

⊢ ∀f1 f2.
    abs_rat f1 = abs_rat f2 ⇔
    frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

⊢ ∀r1. r1 = 0 ⇔ rat_nmr r1 = 0

⊢ ∀f1 f2. rat_equiv f1 f2 ⇔ rat_equiv f1 = rat_equiv f2

⊢ ∀a. rat_equiv a =
      (λx.
           ∃b c.
             0 < b ∧ 0 < c ∧
             frac_mul a (abs_frac (b,b)) = frac_mul x (abs_frac (c,c)))

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a > 0 ⇔ frac_nmr b > 0)

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a < 0 ⇔ frac_nmr b < 0)

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a = 0 ⇔ frac_nmr b = 0)

⊢ ∀a. rat_equiv a a

⊢ ∀a b. rat_equiv a b ⇔ rat_equiv b a

⊢ ∀a b c. rat_equiv a b ∧ rat_equiv b c ⇒ rat_equiv a c

⊢ ∀r1 r2. 0 = r1 − r2 ⇔ r1 = r2

⊢ ∀r1 r2. -r1 = -r2 ⇔ r1 = r2

⊢ ∀r1 r2. r1 = r2 ⇔ rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1

⊢ ∀f1 f2.
    abs_rat f1 = abs_rat f2 ⇔
    frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

⊢ ∀r1 r2 r3. r3 + r1 = r3 + r2 ⇔ r1 = r2

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r3 * r1 = r3 * r2 ⇔ r1 = r2)

⊢ (∀n m. &n = &m ⇔ n = m) ∧ (∀n m. &n = -&m ⇔ n = 0 ∧ m = 0) ∧
  (∀n m. -&n = &m ⇔ n = 0 ∧ m = 0) ∧ ∀n m. -&n = -&m ⇔ n = m

⊢ ∀r1 r2 r3. r1 + r3 = r2 + r3 ⇔ r1 = r2

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r1 * r3 = r2 * r3 ⇔ r1 = r2)

⊢ ∀r1 r2. r1 − r2 = 0 ⇔ r1 = r2

⊢ ∀n. (0 < n ⇒ expn 0 n = 0) ∧ expn 0 (SUC n) = 0

⊢ expn 1 n = 1

⊢ expn r (a + b) = expn r a * expn r b

⊢ (expn r n = 0 ⇔ r = 0 ∧ n ≠ 0) ∧ expn 1 n = 1 ∧ expn r 0 = 1 ∧
  expn r 1 = r

⊢ b ≠ 0 ⇒ expn (a / b) n = expn a n / expn b n

⊢ expn r n = 0 ⇔ r = 0 ∧ n ≠ 0

⊢ expn r n = 1 ⇔ r = 1 ∨ r = -1 ∧ EVEN n ∨ n = 0

⊢ r < 0 ⇒ (expn r n = 1 ⇔ r = -1 ∧ EVEN n ∨ n = 0)

⊢ 0 < r ⇒ (expn r n = 1 ⇔ r = 1 ∨ n = 0)

⊢ r ≠ 0 ∧ r ≠ 1 ∧ r ≠ -1 ⇒ (expn r i = expn r j ⇔ i = j)

⊢ 0 < p ∧ 0 < q ∧ 0 < n ⇒ (expn p n < expn q n ⇔ p < q)

⊢ expn (-1) n = if EVEN n then 1 else -1

⊢ expn r (a * b) = expn (expn r a) b

⊢ expn (-r) n = if EVEN n then expn r n else -expn r n

⊢ r < 0 ⇒ (0 < expn r n ⇔ EVEN n) ∧ (expn r n < 0 ⇔ ODD n)

⊢ expn (a * b) n = expn a n * expn b n

⊢ r ≠ 0 ⇒ expn (rat_minv r) n = rat_minv (expn r n)

⊢ r ≠ 0 ⇒ expn r n ≠ 0

⊢ 0 < r ⇒ 0 < expn r n

⊢ r ≠ 0 ∧ b ≤ a ⇒ expn r (a − b) = expn r a / expn r b

⊢ expn r 0 = 1

⊢ expn r 1 = r

⊢ 0 < i ⇒ 0 ** i = 0

⊢ 1 ** i = 1

⊢ r ≠ 0 ∨ 0 ≤ a ∧ 0 ≤ b ⇒ r ** (a + b) = r ** a * r ** b

⊢ r ** 0 = 1 ∧ r ** 1 = r ∧ 1 ** i = 1 ∧ r ** &n = expn r n ∧
  r ** -&n = rat_minv (expn r n)

⊢ b ≠ 0 ∧ (a ≠ 0 ∨ 0 ≤ i) ⇒ (a / b) ** i = a ** i / b ** i

⊢ ∀r i j. r ≠ 0 ∧ r ≠ 1 ∧ r ≠ -1 ⇒ (r ** i = r ** j ⇔ i = j)

⊢ ∀r i j. 1 < r ⇒ (r ** i ≤ r ** j ⇔ i ≤ j)

⊢ 0 < r ∧ 0 < q ∧ 0 < i ⇒ (r ** i < q ** i ⇔ r < q)

⊢ ∀r i j. 1 < r ⇒ (r ** i < r ** j ⇔ i < j)

⊢ -1 ** i = if i % 2 = 0 then 1 else -1

⊢ r ≠ 0 ∨ 0 ≤ a ∧ 0 ≤ b ⇒ r ** (a * b) = (r ** a) ** b

⊢ r ≠ 0 ∨ 0 < i ⇒ -r ** i = if i % 2 = 0 then r ** i else -(r ** i)

⊢ r ** -&n = rat_minv (expn r n)

⊢ r ** &n = expn r n

⊢ a ≠ 0 ∧ b ≠ 0 ∨ 0 ≤ i ⇒ (a * b) ** i = a ** i * b ** i

⊢ r ≠ 0 ⇒ rat_minv r ** i = rat_minv (r ** i)

⊢ r ≠ 0 ⇒ r ** i ≠ 0

⊢ 0 < r ⇒ 0 < r ** i

⊢ ∀r i j. r ≠ 0 ⇒ r ** (i − j) = r ** i / r ** j

⊢ r ** 0 = 1

⊢ r ≠ 0 ⇒ r ** -i = rat_minv (r ** i)

⊢ ∀a b c. c * (a + b) = c * a + c * b

⊢ ∀r1 r2 r3. r2 ≠ 0 ⇒ (r1 / r2 = r3 ⇔ r1 = r2 * r3)

⊢ ∀r1 r2 r3. r2 < 0 ⇒ (r1 / r2 ≤ r3 ⇔ r2 * r3 ≤ r1)

⊢ ∀r1 r2 r3. 0 < r2 ⇒ (r1 / r2 ≤ r3 ⇔ r1 ≤ r2 * r3)

⊢ ∀r1 r2 r3. r2 < 0 ⇒ (r1 / r2 < r3 ⇔ r2 * r3 < r1)

⊢ ∀r1 r2 r3. 0 < r2 ⇒ (r1 / r2 < r3 ⇔ r1 < r2 * r3)

⊢ ∀r1. r1 ≤ 0 ⇔ rat_nmr r1 ≤ 0

⊢ ∀r1 r2. r1 ≤ r2 ∧ r2 ≤ r1 ⇒ r1 = r2

⊢ ∀f1 f2.
    abs_rat f1 ≤ abs_rat f2 ⇔
    frac_nmr f1 * frac_dnm f2 ≤ frac_nmr f2 * frac_dnm f1

⊢ ∀r1 r2 r3. r3 + r1 ≤ r3 + r2 ⇔ r1 ≤ r2

⊢ ∀r1 r2. ¬(r2 < r1) ⇔ r1 ≤ r2

⊢ ∀a b c. a ≤ b ∧ b < c ⇒ a < c

⊢ 0 ≤ a ∧ a ≤ b ∧ 0 ≤ c ∧ c ≤ d ⇒ a * c ≤ b * d

⊢ ∀r1 r2 r3. r1 + r3 ≤ r2 + r3 ⇔ r1 ≤ r2

⊢ ∀r1. r1 ≤ r1

⊢ ∀r1 r2 r3. r1 ≤ r2 ∧ r2 ≤ r3 ⇒ r1 ≤ r3

⊢ ∀r1 r2. r1 < 0 ⇒ r2 ≤ 0 ⇒ r1 + r2 < 0

⊢ ∀r1 r2. r1 < 0 ⇒ r2 < 0 ⇒ r1 + r2 < 0

⊢ ∀r1. r1 < 0 ⇔ rat_nmr r1 < 0

⊢ 0 < 1

⊢ ∀r1 r2. 0 < r1 − r2 ⇔ r2 < r1

⊢ ∀r1 r2. -r1 < -r2 ⇔ r2 < r1

⊢ ∀r1 r2. r1 < -r2 ⇔ r2 < -r1

⊢ ∀r1 r2. r1 < r2 ⇒ ¬(r2 < r1)

⊢ ∀f1 f2.
    abs_rat f1 < abs_rat f2 ⇔
    frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1

⊢ ∀r1 r2. r1 < r2 ⇒ r1 ≤ r2

⊢ ∀r1 r2. r1 < r2 ⇒ r1 ≠ r2

⊢ ∀r1 r2 r3. r3 + r1 < r3 + r2 ⇔ r1 < r2

⊢ ∀r1 r2. ¬(r2 ≤ r1) ⇔ r1 < r2

⊢ ∀r1 r2. r1 < r2 ⇔ r1 ≤ r2 ∧ ¬(r2 ≤ r1)

⊢ ∀a b c. a < b ∧ b ≤ c ⇒ a < c

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r3 * r2 < r3 * r1 ⇔ r1 < r2)

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r3 * r1 < r3 * r2 ⇔ r1 < r2)

⊢ 0 < r ∧ 1 < q ⇒ r < r * q

⊢ ∀r1 r2 r3. r1 + r3 < r2 + r3 ⇔ r1 < r2

⊢ ∀r1. ¬(r1 < r1)

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r2 * r3 < r1 * r3 ⇔ r1 < r2)

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 * r3 < r2 * r3 ⇔ r1 < r2)

⊢ ∀r1 r2. r1 − r2 < 0 ⇔ r1 < r2

⊢ ∀r1 r2. r1 < r2 ∨ r1 = r2 ∨ r2 < r1

⊢ ∀r1 r2 r3. r1 < r2 ∧ r2 < r3 ⇒ r1 < r3

⊢ (&a ≤ &b ⇔ a ≤ b) ∧ (-&m ≤ &n ⇔ T) ∧ (&m ≤ -&n ⇔ m = 0 ∧ n = 0) ∧
  (-&m ≤ -&n ⇔ n ≤ m)

⊢ ∀r1 r2 r3. r1 − r2 = r3 ⇔ r1 = r2 + r3

⊢ ∀r1 r2 r3. r1 − r2 ≤ r3 ⇔ r1 ≤ r2 + r3

⊢ ∀r1 r2 r3. r1 − r2 < r3 ⇔ r1 < r2 + r3

⊢ a < b ⇔ a ≤ b ∧ a ≠ b

⊢ 0 < a ∧ a < c ∧ 0 < b ∧ b < d ⇒ a * b < c * d

⊢ (&a < &b ⇔ a < b) ∧ (-&m < &n ⇔ 0 < m ∨ 0 < n) ∧ (&m < -&n ⇔ F) ∧
  (-&m < -&n ⇔ n < m)

⊢ rat_minv 1 = 1

⊢ ∀f1. 0 ≠ frac_nmr f1 ⇒ rat_minv (abs_rat f1) = abs_rat (frac_minv f1)

⊢ ∀x. frac_nmr x ≠ 0 ⇒
      abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x)

⊢ a ≠ 0 ∧ b ≠ 0 ⇒ rat_minv (a / b) = rat_minv a / rat_minv b

⊢ r ≠ 0 ⇒ rat_minv r ≠ 0

⊢ r ≠ 0 ⇒ (rat_minv r = r ⇔ r = 1 ∨ r = -1 ∨ r = 0)

⊢ ∀r1. r1 ≠ 0 ⇒ (rat_minv r1 < 0 ⇔ r1 < 0) ∧ (0 < rat_minv r1 ⇔ 0 < r1)

⊢ ∀r. 0 < r ⇒ (1 < rat_minv r ⇔ r < 1) ∧ (rat_minv r < 1 ⇔ 1 < r)

⊢ ∀r. r < 0 ⇒ (-1 < rat_minv r ⇔ r < -1) ∧ (rat_minv r < -1 ⇔ -1 < r)

⊢ a ≠ 0 ∧ b ≠ 0 ⇒ rat_minv (a * b) = rat_minv a * rat_minv b

⊢ r ≠ 0 ⇒
  rat_minv r = rat_of_int (RAT_SGN r) * &RATD r / rat_of_int (ABS (RATN r))

⊢ r ≠ 0 ⇒ rat_minv (rat_minv r) = r

⊢ ∀a b c. a * (b * c) = a * b * c

⊢ ∀f1 f2. abs_rat f1 * abs_rat f2 = abs_rat (frac_mul f1 f2)

⊢ ∀a b. a * b = b * a

⊢ (∀x y.
     abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)) ∧
  ∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)

⊢ ∀x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)

⊢ ∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)

⊢ ∀a. 1 * a = a

⊢ ∀a. a ≠ 0 ⇒ rat_minv a * a = 1

⊢ ∀r1. 0 * r1 = 0

⊢ -a * -b = a * b

⊢ (∀n m. &n * &m = &(n * m)) ∧ (∀n m. -&n * &m = -&(n * m)) ∧
  (∀n m. &n * -&m = -&(n * m)) ∧ ∀n m. -&n * -&m = &(n * m)

⊢ ∀r1. r1 ≠ 0 ⇔ ONE_ONE ($* r1)

⊢ ∀a. a * 1 = a

⊢ ∀a. a ≠ 0 ⇒ a * rat_minv a = 1

⊢ ∀r1. r1 * 0 = 0

⊢ ∀p q.
    (0 < p * q ⇔ 0 < p ∧ 0 < q ∨ p < 0 ∧ q < 0) ∧
    (p * q < 0 ⇔ 0 < p ∧ q < 0 ∨ p < 0 ∧ 0 < q)

⊢ abs_rat (abs_frac (frac_nmr f1,frac_dnm f1)) = 1 ⇔
  frac_nmr f1 = frac_dnm f1

⊢ ∀f1. frac_nmr (rep_rat (abs_rat f1)) = 0 ⇔ frac_nmr f1 = 0

⊢ ∀f1. 0 < frac_nmr (rep_rat (abs_rat f1)) ⇔ 0 < frac_nmr f1

⊢ ∀f1. frac_nmr (rep_rat (abs_rat f1)) < 0 ⇔ frac_nmr f1 < 0

⊢ ∀a b. frac_nmr a = 0 ⇒ (rat_equiv a b ⇔ frac_nmr b = 0)

⊢ ∀r1 r2. r1 * r2 = r2 ⇔ r1 = 1 ∨ r2 = 0

⊢ ∀r1 r2. r1 = 0 ∨ r2 = 0 ⇔ r1 * r2 = 0

⊢ ∀r1 r2. r1 * r2 ≠ 0 ⇔ r1 ≠ 0 ∧ r2 ≠ 0

⊢ ∀r1 r2. r1 * r2 = 0 ⇔ r1 = 0 ∨ r2 = 0

⊢ ∀i. rat_of_int i = abs_rat (abs_frac (i,1))

⊢ ∀n. 0 = rat_0 ∧ ∀n. &SUC n = &n + rat_1

⊢ ∀n1. &n1 = abs_rat (abs_frac (&n1,1))

⊢ &a ≤ &b ⇔ a ≤ b

⊢ &a < &b ⇔ a < b

⊢ ∀a b c. (a + b) * c = a * c + b * c

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r1 = r2 / r3 ⇔ r1 * r3 = r2)

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r1 ≤ r2 / r3 ⇔ r2 ≤ r1 * r3)

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 ≤ r2 / r3 ⇔ r1 * r3 ≤ r2)

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r1 < r2 / r3 ⇔ r2 < r1 * r3)

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 < r2 / r3 ⇔ r1 * r3 < r2)

⊢ ∀r1 r2 r3. r1 = r2 − r3 ⇔ r1 + r3 = r2

⊢ ∀r1 r2 r3. r1 ≤ r2 − r3 ⇔ r1 + r3 ≤ r2

⊢ ∀r1 r2 r3. r1 < r2 − r3 ⇔ r1 + r3 < r2

⊢ ∀r1. ∃a1 b1. r1 = abs_rat (frac_save a1 b1)

⊢ ∀a1 b1.
    abs_rat (frac_save a1 b1) ≠ 0 ⇒
    rat_minv (abs_rat (frac_save a1 b1)) =
    abs_rat (frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 − 1)))

⊢ ∀n. &n = abs_rat (frac_save (&n) 0)

⊢ ∀a1 b1. abs_rat (frac_save a1 b1) = a1 // (&b1 + 1)

⊢ RAT_SGN 0 = 0

⊢ ∀r1. -RAT_SGN (-r1) = RAT_SGN r1

⊢ RAT_SGN (-r) = -RAT_SGN r

⊢ RAT_SGN (-r) = -RAT_SGN r

⊢ RAT_SGN r = SGN (RATN r)

⊢ RAT_SGN (abs_rat f1) = frac_sgn f1

⊢ ∀r1.
    (RAT_SGN r1 = -1 ⇔ r1 < 0) ∧ (RAT_SGN r1 = 0 ⇔ r1 = 0) ∧
    (RAT_SGN r1 = 1 ⇔ r1 > 0)

⊢ ∀r1.
    (RAT_SGN r1 ≠ -1 ⇔ RAT_SGN r1 = 0 ∨ RAT_SGN r1 = 1) ∧
    (RAT_SGN r1 ≠ 0 ⇔ RAT_SGN r1 = -1 ∨ RAT_SGN r1 = 1) ∧
    (RAT_SGN r1 ≠ 1 ⇔ RAT_SGN r1 = -1 ∨ RAT_SGN r1 = 0)

⊢ ∀f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1

⊢ d ≠ 0 ⇒ RAT_SGN (n / d) = RAT_SGN n * RAT_SGN d

⊢ (RAT_SGN r = 0 ⇔ r = 0) ∧ (0 = RAT_SGN r ⇔ r = 0)

⊢ ∀r1. r1 ≠ 0 ⇒ RAT_SGN (rat_minv r1) = RAT_SGN r1

⊢ ∀r1 r2. RAT_SGN (r1 * r2) = RAT_SGN r1 * RAT_SGN r2

⊢ RAT_SGN r = -1 ⇔ r < 0

⊢ RAT_SGN (&NUMERAL (BIT1 n)) = 1 ∧ RAT_SGN (&NUMERAL (BIT2 n)) = 1

⊢ RAT_SGN (&n) = if n = 0 then 0 else 1

⊢ RAT_SGN r = 1 ⇔ 0 < r

⊢ ∀r1. RAT_SGN r1 = -1 ∨ RAT_SGN r1 = 0 ∨ RAT_SGN r1 = 1

⊢ ∀r1 r2. r1 − r2 = r1 + -r2

⊢ ∀f1 f2. abs_rat f1 − abs_rat f2 = abs_rat (frac_sub f1 f2)

⊢ (∀x y.
     abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)) ∧
  ∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)

⊢ ∀x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)

⊢ ∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)

⊢ ∀r. r − r = 0

⊢ ∀a b c. c * (a − b) = c * a − c * b

⊢ ∀r1. 0 − r1 = -r1

⊢ ∀a b c. (a − b) * c = a * c − b * c

⊢ ∀r1. r1 − 0 = r1

⊢ 2 * x = x + x

⊢ r1 * (r2 / r3) = r1 * r2 / r3

⊢ div_gcd a b = (n,d) ∧ b ≠ 0 ⇒
  rat_of_int a / &b = rat_of_int n / &d ∧ RATN (rat_of_int a / &b) = n ∧
  RATD (rat_of_int a / &b) = d

⊢ div_gcd a b = (n,d) ∧ b ≠ 0 ⇒ d ≠ 0 ∧ coprime (Num n) d ∧ a * &d = n * &b

⊢ frac_dnm f ≠ 0

⊢ coprime (Num (RATN r)) (RATD r)

⊢ 0 = abs_rat frac_0

⊢ 1 = abs_rat frac_1

⊢ (∀a. abs_rat_CLASS (rep_rat_CLASS a) = a) ∧
  ∀c. (∃r. rat_equiv r r ∧ c = rat_equiv r) ⇔
      rep_rat_CLASS (abs_rat_CLASS c) = c

⊢ QUOTIENT rat_equiv abs_rat rep_rat

⊢ QUOTIENT rat_equiv abs_rat rep_rat

⊢ rat_equiv (rep_rat (abs_rat f)) f

⊢ rat_equiv (rep_rat r1) (rep_rat r2) ⇔ r1 = r2

⊢ (∀r. expn r 0 = 1) ∧
  (∀r n. expn r (NUMERAL (BIT1 n)) = r * expn r (NUMERAL (BIT1 n) − 1)) ∧
  ∀r n. expn r (NUMERAL (BIT2 n)) = r * expn r (NUMERAL (BIT1 n))

⊢ rat_of_int i1 = rat_of_int i2 ⇔ i1 = i2

⊢ rat_of_int x + rat_of_int y = rat_of_int (x + y)

⊢ (rat_of_int i = &n ⇔ i = &n) ∧ (&n = rat_of_int i ⇔ i = &n)

⊢ rat_of_int i ≤ rat_of_int j ⇔ i ≤ j

⊢ rat_of_int i < rat_of_int j ⇔ i < j

⊢ rat_of_int x * rat_of_int y = rat_of_int (x * y)

⊢ rat_of_int (-i) = -rat_of_int i

⊢ rat_of_int (frac_nmr (rep_rat q)) / rat_of_int (frac_dnm (rep_rat q)) = q

⊢ rat_of_int (&x) = &x

⊢ 0 = rat_0 ∧ &SUC 0 = rat_1 ∧
  (∀n. &SUC (NUMERAL (BIT1 n)) = &NUMERAL (BIT1 n) + rat_1) ∧
  ∀n. &SUC (NUMERAL (BIT2 n)) = &NUMERAL (BIT2 n) + rat_1

⊢ 0 = rat_0 ∧ &SUC 0 = rat_1 ∧ ∀n. &SUC (SUC n) = &SUC n + rat_1

⊢ ∀P. P 0 ∧ P (SUC 0) ∧ (∀n. P (SUC n) ⇒ P (SUC (SUC n))) ⇒ ∀v. P v

⊢ (∀a. abs_rat (rep_rat a) = a) ∧
  ∀r s. rat_equiv r s ⇔ abs_rat r = abs_rat s

⊢ ∀i. ∃j. 0 < j ∧ rep_rat (rat_of_int i) = abs_frac (j * i,j)