gcd_fractions: THEORY
%------------------------------------------------------------------------------
% Author: Alfons Geser, HTWK Leipzig, Germany
% Date: May, 2009
%------------------------------------------------------------------------------
BEGIN

  IMPORTING gcd

  p, q, k: VAR posint
  r: VAR posrat

  div_by_gcd_prep: LEMMA FORALL (p: posint, q: posint):
    integer_pred(p / gcd(p, q)) AND p / gcd(p, q) >= 0 AND p / gcd(p, q) > 0;


  div_by_gcd(p, q): posint = p / gcd(p, q)

  gcd_div_by_gcd: LEMMA gcd(div_by_gcd(p, q), div_by_gcd(q, p)) = 1

  quotient_fully_cancelled: THEOREM
    EXISTS p, q: gcd(p, q) = 1 AND r = p / q

END gcd_fractions