num-and-denom-helper

Included Books

basic-arithmetic inequalities prefer-times non-linear

other

(in-package "ACL2")

local

(local (include-book "basic-arithmetic"))

local

(local (include-book "inequalities"))

local

(local (include-book "prefer-times"))

local

(local (include-book "non-linear"))

nonneg-int-modfunction

(defun nonneg-int-mod
  (n d)
  (declare (xargs :guard (and (integerp n) (>= n 0) (integerp d) (< 0 d))))
  (if (zp d)
    (nfix n)
    (if (< (nfix n) d)
      (nfix n)
      (nonneg-int-mod (- n d) d))))

nonneg-int-mod-<-divisortheorem

(defthm nonneg-int-mod-<-divisor
  (implies (and (integerp d) (< 0 d))
    (< (nonneg-int-mod n d) d))
  :rule-classes :linear)

nonneg-int-mod-nonnegative-integer-quotienttheorem

(defthm nonneg-int-mod-nonnegative-integer-quotient
  (equal (+ (nonneg-int-mod n d)
      (* (nfix d) (nonnegative-integer-quotient n d)))
    (nfix n))
  :rule-classes ((:elim :corollary (implies (and (integerp n) (integerp d) (>= n 0) (>= d 0))
       (equal (+ (nonneg-int-mod n d)
           (* d (nonnegative-integer-quotient n d)))
         n)))))

nonneg-int-mod-0theorem

(defthm nonneg-int-mod-0
  (equal (nonneg-int-mod 0 d) 0)
  :hints (("Goal" :use (:instance nonneg-int-mod-nonnegative-integer-quotient
       (n 0)))))

local

(local (defun induct-on-nonneg-int
    (j)
    (if (zp j)
      t
      (induct-on-nonneg-int (- j 1)))))

hacktheorem

(defthm hack (equal (* -1 x) (- x)))

nonneg-int-mod-+-*theorem

(defthm nonneg-int-mod-+-*
  (implies (and (integerp j)
      (integerp n)
      (integerp x)
      (>= x 0)
      (< x n)
      (>= j 0))
    (equal (nonneg-int-mod (+ x (* j n)) n) x))
  :hints (("Goal" :induct (induct-on-nonneg-int j))))

nonneg-int-mod-+-*-nonneg-int-modtheorem

(defthm nonneg-int-mod-+-*-nonneg-int-mod
  (implies (and (integerp j)
      (integerp n)
      (integerp x)
      (>= j 0)
      (< 0 n)
      (>= x 0))
    (equal (nonneg-int-mod (+ x (* j n)) n)
      (nonneg-int-mod x n))))

nonneg-int-mod-+-*-nonneg-int-mod-1theorem

(defthm nonneg-int-mod-+-*-nonneg-int-mod-1
  (implies (and (integerp j)
      (integerp k)
      (integerp n)
      (integerp x)
      (>= j 0)
      (>= k 0)
      (< 0 n)
      (>= x 0)
      (equal (nonneg-int-mod k n) 0))
    (equal (nonneg-int-mod (+ x (* j k)) n)
      (nonneg-int-mod x n)))
  :hints (("Goal" :in-theory (disable nonneg-int-mod-+-*-nonneg-int-mod)
     :use (:instance nonneg-int-mod-+-*-nonneg-int-mod
       (j (* j (nonnegative-integer-quotient k n)))))))

divisor-nonnegative-integer-quotienttheorem

(defthm divisor-nonnegative-integer-quotient
  (implies (equal (nonneg-int-mod n d) 0)
    (equal (* (nfix d) (nonnegative-integer-quotient n d))
      (nfix n)))
  :rule-classes nil)

left-nonneg-int-mod-*theorem

(defthm left-nonneg-int-mod-*
  (implies (and (integerp j) (integerp n) (>= n 0))
    (equal (nonneg-int-mod (* j n) n) 0))
  :hints (("Goal" :induct (induct-on-nonneg-int j))))

right-nonneg-int-mod-*theorem

(defthm right-nonneg-int-mod-*
  (implies (and (integerp j) (integerp n) (>= n 0))
    (equal (nonneg-int-mod (* n j) n) 0)))

nonneg-int-mod-*-0theorem

(defthm nonneg-int-mod-*-0
  (implies (and (integerp j)
      (integerp y)
      (>= j 0)
      (equal (nonneg-int-mod j n) 0))
    (equal (nonneg-int-mod (* j y) n) 0))
  :hints (("Goal" :in-theory (disable right-nonneg-int-mod-*)
     :use ((:instance right-nonneg-int-mod-*
        (j (* y (nonnegative-integer-quotient j n))))))))

nonneg-int-mod-+-0theorem

(defthm nonneg-int-mod-+-0
  (implies (and (integerp x)
      (>= x 0)
      (>= y 0)
      (equal (nonneg-int-mod x n) 0)
      (equal (nonneg-int-mod y n) 0))
    (equal (nonneg-int-mod (+ x y) n) 0)))

nonneg-int-mod-minus-0theorem

(defthm nonneg-int-mod-minus-0
  (implies (and (integerp x)
      (integerp y)
      (>= y 0)
      (equal (nonneg-int-mod x n) 0)
      (equal (nonneg-int-mod y n) 0))
    (equal (nonneg-int-mod (- x y) n) 0))
  :hints (("Goal" :in-theory (disable right-nonneg-int-mod-*)
     :use (:instance right-nonneg-int-mod-*
       (j (- (nonnegative-integer-quotient x n)
           (nonnegative-integer-quotient y n)))))))

linear-combination-nonneg-int-modtheorem

(defthm linear-combination-nonneg-int-mod
  (implies (and (integerp a)
      (integerp b)
      (integerp x)
      (integerp y)
      (>= a 0)
      (>= b 0)
      (equal (nonneg-int-mod a n) 0)
      (equal (nonneg-int-mod b n) 0))
    (equal (nonneg-int-mod (+ (* a x) (* b y)) n) 0))
  :hints (("Goal" :in-theory (disable nonneg-int-mod-minus-0)
     :use ((:instance nonneg-int-mod-minus-0
        (x (* a x))
        (y (* b (- y)))) (:instance nonneg-int-mod-*-0 (j b) (y (- y)))
       (:instance nonneg-int-mod-minus-0
         (x (* b y))
         (y (* a (- x))))
       (:instance nonneg-int-mod-*-0 (j a) (y (- x)))))))

divisor-<=theorem

(defthm divisor-<=
  (implies (and (integerp n) (> n 0) (equal (nonneg-int-mod n d) 0))
    (<= d n)))

in-theory

(in-theory (disable divisor-<=))

nonneg-int-mod-1theorem

(defthm nonneg-int-mod-1 (equal (nonneg-int-mod n 1) 0))

nonneg-int-gcdfunction

(defun nonneg-int-gcd
  (x y)
  (declare (xargs :guard (and (integerp x) (>= x 0) (integerp y) (>= y 0))))
  (if (zp y)
    (nfix x)
    (nonneg-int-gcd y (nonneg-int-mod x y))))

nonneg-int-gcd->-0theorem

(defthm nonneg-int-gcd->-0
  (implies (or (and (integerp d) (> d 0)) (and (integerp n) (> n 0)))
    (> (nonneg-int-gcd n d) 0))
  :rule-classes :type-prescription)

nonneg-int-gcd-is-common-divisortheorem

(defthm nonneg-int-gcd-is-common-divisor
  (and (equal (nonneg-int-mod x (nonneg-int-gcd x y)) 0)
    (equal (nonneg-int-mod y (nonneg-int-gcd x y)) 0)))

nonneg-int-gcd-multiplier1mutual-recursion

(mutual-recursion (defun nonneg-int-gcd-multiplier1
    (x y)
    (declare (xargs :guard (and (integerp x) (integerp y) (>= x 0) (>= y 0))))
    (if (zp y)
      1
      (nonneg-int-gcd-multiplier2 y (nonneg-int-mod x y))))
  (defun nonneg-int-gcd-multiplier2
    (x y)
    (declare (xargs :guard (and (integerp x) (integerp y) (>= x 0) (>= y 0))))
    (if (zp y)
      0
      (+ (nonneg-int-gcd-multiplier1 y (nonneg-int-mod x y))
        (- (* (nonneg-int-gcd-multiplier2 y (nonneg-int-mod x y))
            (nonnegative-integer-quotient x y)))))))

linear-combination-for-nonneg-int-gcdtheorem

(defthm linear-combination-for-nonneg-int-gcd
  (equal (nonneg-int-gcd x y)
    (+ (* (nfix x) (nonneg-int-gcd-multiplier1 x y))
      (* (nfix y) (nonneg-int-gcd-multiplier2 x y)))))

in-theory

(in-theory (disable linear-combination-for-nonneg-int-gcd))

nonneg-int-gcd-is-largest-common-divisor-modtheorem

(defthm nonneg-int-gcd-is-largest-common-divisor-mod
  (implies (and (equal (nonneg-int-mod x d) 0)
      (equal (nonneg-int-mod y d) 0))
    (equal (nonneg-int-mod (nonneg-int-gcd x y) d) 0))
  :hints (("Goal" :in-theory (enable linear-combination-for-nonneg-int-gcd))))

nonneg-int-gcd-is-largest-common-divisor-<=theorem

(defthm nonneg-int-gcd-is-largest-common-divisor-<=
  (implies (and (or (and (integerp x) (> x 0)) (and (integerp y) (> y 0)))
      (equal (nonneg-int-mod x d) 0)
      (equal (nonneg-int-mod y d) 0))
    (<= d (nonneg-int-gcd x y)))
  :hints (("Goal" :in-theory (enable divisor-<=))))

nonnegative-integer-quotient-gcdtheorem

(defthm nonnegative-integer-quotient-gcd
  (implies (and (integerp x) (integerp y) (>= x 0) (>= y 0))
    (and (equal (* (nonneg-int-gcd x y)
          (nonnegative-integer-quotient x (nonneg-int-gcd x y)))
        x)
      (equal (* (nonneg-int-gcd x y)
          (nonnegative-integer-quotient y (nonneg-int-gcd x y)))
        y)))
  :hints (("Goal" :use ((:instance divisor-nonnegative-integer-quotient
        (n x)
        (d (nonneg-int-gcd x y))) (:instance divisor-nonnegative-integer-quotient
         (n y)
         (d (nonneg-int-gcd x y)))))))

linear-combination-gcd=1theorem

(defthm linear-combination-gcd=1
  (implies (and (integerp x) (equal (nonneg-int-gcd y z) 1))
    (equal (+ (* x y (nonneg-int-gcd-multiplier1 y z))
        (* x z (nonneg-int-gcd-multiplier2 y z)))
      x)))

divisor-of-product-divides-factortheorem

(defthm divisor-of-product-divides-factor
  (implies (and (equal (nonneg-int-mod (* x y) z) 0)
      (equal (nonneg-int-gcd y z) 1)
      (integerp x)
      (integerp y)
      (>= x 0)
      (>= y 0))
    (equal (nonneg-int-mod x z) 0))
  :rule-classes nil
  :hints (("Goal" :use ((:instance linear-combination-nonneg-int-mod
        (a (* x y))
        (b z)
        (n z)
        (x (nonneg-int-gcd-multiplier1 y z))
        (y (* x (nonneg-int-gcd-multiplier2 y z))))))))

nonneg-int-mod-abs-+-*theorem

(defthm nonneg-int-mod-abs-+-*
  (implies (and (integerp j) (integerp n) (integerp x) (<= 0 n))
    (equal (nonneg-int-mod (abs (+ x (* j n)))
        (nonneg-int-gcd (abs x) n))
      0))
  :rule-classes ((:rewrite :corollary (implies (and (integerp j)
         (integerp n)
         (integerp x)
         (<= 0 n)
         (<= (+ x (* j n)) 0)
         (<= x 0))
       (equal (nonneg-int-mod (+ (- x) (- (* j n)))
           (nonneg-int-gcd (- x) n))
         0))
     :hints (("Goal" :cases ((< (+ x (* j n)) 0))))) (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (<= 0 n)
          (<= 0 (+ x (* j n)))
          (<= x 0))
        (equal (nonneg-int-mod (+ x (* j n)) (nonneg-int-gcd (- x) n))
          0)))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (<= 0 n)
          (<= (+ x (* j n)) 0)
          (<= 0 x))
        (equal (nonneg-int-mod (+ (- x) (- (* j n))) (nonneg-int-gcd x n))
          0)))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (<= 0 n)
          (<= 0 (+ x (* j n)))
          (<= 0 x))
        (equal (nonneg-int-mod (+ x (* j n)) (nonneg-int-gcd x n))
          0))))
  :hints (("Subgoal 4" :use (:instance linear-combination-nonneg-int-mod
       (a (- x))
       (b n)
       (x 1)
       (y (- j))
       (n (nonneg-int-gcd (- x) n)))) ("Subgoal 3" :use (:instance linear-combination-nonneg-int-mod
        (a (- x))
        (b n)
        (x -1)
        (y j)
        (n (nonneg-int-gcd (- x) n))))
    ("Subgoal 2" :use (:instance linear-combination-nonneg-int-mod
        (a x)
        (b n)
        (x -1)
        (y (- j))
        (n (nonneg-int-gcd x n))))
    ("Subgoal 1" :use (:instance linear-combination-nonneg-int-mod
        (a x)
        (b n)
        (x 1)
        (y j)
        (n (nonneg-int-gcd x n))))))

nonneg-int-gcd-abs->=theorem

(defthm nonneg-int-gcd-abs->=
  (implies (and (integerp j) (integerp n) (integerp x) (< 0 n))
    (>= (nonneg-int-gcd (abs (+ x (* j n))) n)
      (nonneg-int-gcd (abs x) n)))
  :rule-classes nil)

nonneg-int-mod-abstheorem

(defthm nonneg-int-mod-abs
  (implies (and (integerp j) (integerp n) (integerp x) (< 0 n))
    (equal (nonneg-int-mod (abs x)
        (nonneg-int-gcd (abs (+ x (* j n))) n))
      0))
  :rule-classes ((:rewrite :corollary (implies (and (integerp j)
         (integerp n)
         (integerp x)
         (<= 0 n)
         (<= (+ x (* j n)) 0)
         (<= x 0))
       (equal (nonneg-int-mod (- x)
           (nonneg-int-gcd (+ (- x) (- (* j n))) n))
         0))) (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= 0 (+ x (* j n)))
          (<= x 0))
        (equal (nonneg-int-mod (- x) (nonneg-int-gcd (+ x (* j n)) n))
          0)))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= (+ x (* j n)) 0)
          (<= 0 x))
        (equal (nonneg-int-mod x (nonneg-int-gcd (+ (- x) (- (* j n))) n))
          0)))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= 0 (+ x (* j n)))
          (<= 0 x))
        (equal (nonneg-int-mod x (nonneg-int-gcd (+ x (* j n)) n))
          0))))
  :hints (("Subgoal 4" :use (:instance linear-combination-nonneg-int-mod
       (a (+ (- x) (- (* j n))))
       (b n)
       (x 1)
       (y j)
       (n (nonneg-int-gcd (+ (- x) (- (* j n))) n)))) ("Subgoal 3" :use (:instance linear-combination-nonneg-int-mod
        (a (+ (- x) (- (* j n))))
        (b n)
        (x -1)
        (y (- j))
        (n (nonneg-int-gcd (+ (- x) (- (* j n))) n))))
    ("Subgoal 2" :use (:instance linear-combination-nonneg-int-mod
        (a (+ x (* j n)))
        (b n)
        (x -1)
        (y j)
        (n (nonneg-int-gcd (+ x (* j n)) n))))
    ("Subgoal 1" :use (:instance linear-combination-nonneg-int-mod
        (a (+ x (* j n)))
        (b n)
        (x 1)
        (y (- j))
        (n (nonneg-int-gcd (+ x (* j n)) n))))))

nonneg-int-gcd-abs-<=theorem

(defthm nonneg-int-gcd-abs-<=
  (implies (and (integerp j) (integerp n) (integerp x) (< 0 n))
    (<= (nonneg-int-gcd (abs (+ x (* j n))) n)
      (nonneg-int-gcd (abs x) n)))
  :rule-classes nil)

nonneg-int-gcd-abstheorem

(defthm nonneg-int-gcd-abs
  (implies (and (integerp j) (integerp n) (integerp x) (< 0 n))
    (equal (nonneg-int-gcd (abs (+ x (* j n))) n)
      (nonneg-int-gcd (abs x) n)))
  :rule-classes ((:rewrite :corollary (implies (and (integerp j)
         (integerp n)
         (integerp x)
         (< 0 n)
         (<= (+ x (* j n)) 0)
         (<= x 0))
       (equal (nonneg-int-gcd (+ (- x) (- (* j n))) n)
         (nonneg-int-gcd (- x) n)))
     :hints (("Goal" :cases ((< (+ x (* j n)) 0))))) (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= 0 (+ x (* j n)))
          (<= x 0))
        (equal (nonneg-int-gcd (+ x (* j n)) n)
          (nonneg-int-gcd (- x) n))))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= (+ x (* j n)) 0)
          (<= 0 x))
        (equal (nonneg-int-gcd (+ (- x) (- (* j n))) n)
          (nonneg-int-gcd x n))))
    (:rewrite :corollary (implies (and (integerp j)
          (integerp n)
          (integerp x)
          (< 0 n)
          (<= 0 (+ x (* j n)))
          (<= 0 x))
        (equal (nonneg-int-gcd (+ x (* j n)) n)
          (nonneg-int-gcd x n)))))
  :hints (("Goal" :in-theory (disable nonneg-int-mod-abs-+-* nonneg-int-mod-abs)
     :use (nonneg-int-gcd-abs->= nonneg-int-gcd-abs-<=))))

commutativity-of-nonneg-int-gcdtheorem

(defthm commutativity-of-nonneg-int-gcd
  (implies (and (integerp x) (integerp y) (>= x 0) (>= y 0))
    (equal (nonneg-int-gcd x y) (nonneg-int-gcd y x)))
  :hints (("Goal" :cases ((< x y) (> x y)))))

cross-product-factortheorem

(defthm cross-product-factor
  (implies (and (equal (nonneg-int-gcd a b) 1)
      (equal (* a d) (* b c))
      (integerp a)
      (integerp b)
      (integerp c)
      (integerp d)
      (>= a 0)
      (>= b 0)
      (>= c 0)
      (>= d 0))
    (and (equal (nonneg-int-mod c a) 0)
      (equal (nonneg-int-mod d b) 0)))
  :rule-classes nil
  :hints (("Goal" :use ((:instance divisor-of-product-divides-factor
        (x c)
        (y b)
        (z a)) (:instance divisor-of-product-divides-factor
         (x d)
         (y a)
         (z b))))))

nonneg-int-gcd-1-righttheorem

(defthm nonneg-int-gcd-1-right
  (equal (nonneg-int-gcd x 1) 1))

nonneg-int-gcd-1-lefttheorem

(defthm nonneg-int-gcd-1-left
  (implies (and (integerp x) (>= x 0))
    (equal (nonneg-int-gcd 1 x) 1))
  :rule-classes ((:rewrite :corollary (equal (nonneg-int-gcd 1 x) 1)))
  :hints (("Goal" :in-theory (disable nonneg-int-gcd-1-right)
     :use nonneg-int-gcd-1-right)))

nonneg-int-gcd-numerator-denominatortheorem

(defthm nonneg-int-gcd-numerator-denominator
  (equal (nonneg-int-gcd (abs (numerator x)) (denominator x))
    1)
  :rule-classes ((:rewrite :corollary (implies (>= (numerator x) 0)
       (equal (nonneg-int-gcd (denominator x) (numerator x)) 1))) (:rewrite :corollary (implies (<= (numerator x) 0)
        (equal (nonneg-int-gcd (denominator x) (- (numerator x))) 1))))
  :hints (("Goal" :use (:instance lowest-terms
       (n (nonneg-int-gcd (abs (numerator x)) (denominator x)))
       (r (* (signum (numerator x))
           (nonnegative-integer-quotient (abs (numerator x))
             (nonneg-int-gcd (abs (numerator x)) (denominator x)))))
       (q (nonnegative-integer-quotient (denominator x)
           (nonneg-int-gcd (abs (numerator x)) (denominator x))))))))

lowest-terms-nonneg-int-modtheorem

(defthm lowest-terms-nonneg-int-mod
  (implies (and (integerp n1)
      (integerp n2)
      (integerp d1)
      (integerp d2)
      (> d1 0)
      (> d2 0)
      (equal (nonneg-int-gcd (abs n1) d1) 1)
      (equal (* (/ d1) n1) (* (/ d2) n2)))
    (and (equal (nonneg-int-mod d2 d1) 0)
      (equal (nonneg-int-mod (abs n2) (abs n1)) 0)))
  :rule-classes nil
  :hints (("Goal" :in-theory (enable prefer-*-to-/)
     :use (:instance cross-product-factor
       (a (abs n1))
       (b d1)
       (c (abs n2))
       (d d2)))))

lowest-terms-<=theorem

(defthm lowest-terms-<=
  (implies (and (integerp n1)
      (integerp n2)
      (integerp d1)
      (integerp d2)
      (> d1 0)
      (> d2 0)
      (equal (nonneg-int-gcd (abs n1) d1) 1)
      (equal (* (/ d1) n1) (* (/ d2) n2)))
    (and (<= d1 d2) (<= (abs n1) (abs n2))))
  :rule-classes nil
  :hints (("Goal" :use lowest-terms-nonneg-int-mod
     :in-theory (enable prefer-*-to-/))))

least-numerator-denominator-nonneg-int-modtheorem

(defthm least-numerator-denominator-nonneg-int-mod
  (implies (and (integerp n) (integerp d) (> d 0))
    (and (equal (nonneg-int-mod d (denominator (* (/ d) n))) 0)
      (equal (nonneg-int-mod (abs n) (abs (numerator (* (/ d) n))))
        0)))
  :rule-classes ((:rewrite :corollary (implies (and (integerp n) (integerp d) (> d 0))
       (equal (nonneg-int-mod d (denominator (* (/ d) n))) 0))) (:rewrite :corollary (implies (and (integerp n) (integerp d) (>= n 0) (> d 0))
        (equal (nonneg-int-mod n (numerator (* (/ d) n))) 0)))
    (:rewrite :corollary (implies (and (integerp n) (integerp d) (<= n 0) (> d 0))
        (equal (nonneg-int-mod (- n) (- (numerator (* (/ d) n)))) 0))))
  :hints (("Goal" :use (:instance lowest-terms-nonneg-int-mod
       (n1 (numerator (* (/ d) n)))
       (d1 (denominator (* (/ d) n)))
       (n2 n)
       (d2 d)))))

least-numerator-denominator-<=theorem

(defthm least-numerator-denominator-<=
  (implies (and (integerp n) (integerp d) (> d 0))
    (and (<= (denominator (* (/ d) n)) d)
      (<= (abs (numerator (* (/ d) n))) (abs n))))
  :rule-classes ((:linear :corollary (implies (and (integerp n) (integerp d) (> d 0))
       (<= (denominator (* (/ d) n)) d))) (:linear :corollary (implies (and (integerp n) (integerp d) (>= n 0) (> d 0))
        (<= (numerator (* (/ d) n)) n)))
    (:linear :corollary (implies (and (integerp n) (integerp d) (<= n 0) (> d 0))
        (<= n (numerator (* (/ d) n))))))
  :hints (("Goal" :in-theory (enable divisor-<=)) ("Subgoal 4" :in-theory (disable <-minus-minus
        divisor-<=
        least-numerator-denominator-nonneg-int-mod)
      :use (divisor-<= least-numerator-denominator-nonneg-int-mod))
    ("Subgoal 1" :cases ((> n 0)))))

unique-rationalptheorem

(defthm unique-rationalp
  (implies (and (integerp n)
      (integerp d)
      (> d 0)
      (equal (nonneg-int-gcd (abs n) d) 1))
    (and (equal (denominator (* (/ d) n)) d)
      (equal (numerator (* (/ d) n)) n)))
  :hints (("Goal" :use (:instance lowest-terms-<=
       (n1 n)
       (d1 d)
       (n2 (numerator (* (/ d) n)))
       (d2 (denominator (* (/ d) n)))))))