[isabelle] quotient_of: missing lemma
recently I had to work with rational numbers which I had to split into denominator and numerator. To this end, quotient_of can be used, but there was one essential lemma missing, namely that the rational number is exactly numerator / denominator.
lemma quotient_of_div: assumes r: "quotient_of r = (n,d)"
shows "r = of_int n / of_int d"
from theI'[OF quotient_of_unique[of r], unfolded r[unfolded quotient_of_def]]
have "r = Fract n d" by simp
thus ?thesis using Fract_of_int_quotient by simp
Perhaps this might be added to the distribution.
This archive was generated by a fusion of
Pipermail (Mailman edition) and