English
Division in ZNum is compatible with integer division: for all n,d, the embedding of n/d into ℤ equals n/d in ℤ; this covers all sign cases by cases.
Русский
Деление в ZNum совместимо с целочисленным делением: для всех n,d внедрение n/d в ℤ равно n/d в ℤ; учтены все случаи знаков.
LaTeX
$$$\forall n,d:\; ((n / d : ZNum) : \mathbb{Z}) = n / d$$$
Lean4
@[simp, norm_cast]
theorem div_to_int : ∀ n d, ((n / d : ZNum) : ℤ) = n / d
| 0, 0 => by simp [Int.ediv_zero]
| 0, pos _ => (Int.zero_ediv _).symm
| 0, neg _ => (Int.zero_ediv _).symm
| pos _, 0 => (Int.ediv_zero _).symm
| neg _, 0 => (Int.ediv_zero _).symm
| pos n, pos d => (Num.cast_toZNum _).trans <| by rw [← Num.to_nat_to_int]; simp
| pos n, neg d => (Num.cast_toZNumNeg _).trans <| by rw [← Num.to_nat_to_int]; simp
| neg n, pos d =>
show -_ = -_ / ↑d
by
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat, Num.div_to_nat]
change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]
rw [d.to_nat_eq_succ_pred]
| neg n, neg d =>
show ↑(PosNum.pred' n / Num.pos d).succ' = -_ / -↑d
by
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat, Num.div_to_nat]
change (Nat.succ (_ / d) : ℤ) = Nat.succ (n.pred' / (d.pred' + 1))
rw [d.to_nat_eq_succ_pred]
