n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % natAbs ↑d) = ↑↑n % ↑d
n : PosNum
d : ZNum
⊢ ↑(Num.pos n % abs d) = ↑(pos n) % ↑d
rw [← Num.to_nat_to_int, cast_pos, Num.mod_to_nat, ← PosNum.to_nat_to_int, abs_to_nat]
no goals
n : PosNum
d : ZNum
⊢ ↑(↑(Num.pos n) % natAbs ↑d) = ↑↑n % ↑d
rfl
n : PosNum
d : ZNum
⊢ subNatNat (natAbs ↑d) (↑(PosNum.pred' n) % natAbs ↑d + 1) = -(↑↑(PosNum.pred' n) + 1) % ↑d
n : PosNum
d : ZNum
⊢ ↑(abs d) - ↑(Num.succ (PosNum.pred' n % abs d)) = ↑(neg n) % ↑d
rw [← Num.to_nat_to_int, cast_neg, ← Num.to_nat_to_int, Num.succ_to_nat, Num.mod_to_nat,
    abs_to_nat, ← Int.subNatNat_eq_coe, n.to_int_eq_succ_pred]
no goals
n : PosNum
d : ZNum
⊢ subNatNat (natAbs ↑d) (↑(PosNum.pred' n) % natAbs ↑d + 1) = -(↑↑(PosNum.pred' n) + 1) % ↑d
rfl