English
Let p, q be rational numbers with q ≥ 0. The embedding of rationals into nonnegative rationals preserves division by a nonnegative denominator: toNNRat(p/q) = toNNRat(p) / toNNRat(q).
Русский
Пусть p, q — рациональные числа и q ≥ 0. Встраивание рациональных чисел в множество ℚ≥0 сохраняет деление на неотрицательный знаменатель: toNNRat(p/q) = toNNRat(p) / toNNRat(q).
LaTeX
$$$\\\\forall p,q \\\\in \\\\mathbb{Q}, \\\\ q \\\ge 0 \\\\implies \\\\operatorname{toNNRat}(p/q) = \\\\operatorname{toNNRat}(p) / \\\\operatorname{toNNRat}(q).$$$
Lean4
theorem toNNRat_div' (hq : 0 ≤ q) : toNNRat (p / q) = toNNRat p / toNNRat q := by
rw [div_eq_inv_mul, div_eq_inv_mul, toNNRat_mul (inv_nonneg.2 hq), toNNRat_inv]
