d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
d n : PosNum
⊢ ↑n / ↑d = ↑(divMod d n).fst ∧ ↑n % ↑d = ↑(divMod d n).snd
rw [Nat.div_mod_unique (PosNum.cast_pos _)]
case one
d : PosNum
⊢ ↑(divMod d one).snd + ↑d * ↑(divMod d one).fst = ↑one ∧ ↑(divMod d one).snd < ↑d

case bit1
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(divMod d (bit1 n)).snd + ↑d * ↑(divMod d (bit1 n)).fst = ↑(bit1 n) ∧ ↑(divMod d (bit1 n)).snd < ↑d

case bit0
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(divMod d (bit0 n)).snd + ↑d * ↑(divMod d (bit0 n)).fst = ↑(bit0 n) ∧ ↑(divMod d (bit0 n)).snd < ↑d
d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
induction' n with n IH n IH
no goals
case one
d : PosNum
⊢ ↑(divMod d one).snd + ↑d * ↑(divMod d one).fst = ↑one ∧ ↑(divMod d one).snd < ↑d
exact
  divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
no goals
d : PosNum
⊢ ↑1 + ↑d * _root_.bit0 ↑0 = ↑one
simp
case bit1
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
        ↑d *
          ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
      ↑(bit1 n) ∧
    ↑(match divMod d n with
          | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
      ↑d
case bit1
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(divMod d (bit1 n)).snd + ↑d * ↑(divMod d (bit1 n)).fst = ↑(bit1 n) ∧ ↑(divMod d (bit1 n)).snd < ↑d
unfold divMod
case bit1
d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d →
    ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
          ↑d *
            ↑(match divMod d n with
                | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
        ↑(bit1 n) ∧
      ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
        ↑d
case bit1
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
        ↑d *
          ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
      ↑(bit1 n) ∧
    ↑(match divMod d n with
          | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
      ↑d
revert IH
case bit1.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
        ↑(bit1 n) ∧
      ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
        ↑d
case bit1
d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d →
    ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
          ↑d *
            ↑(match divMod d n with
                | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
        ↑(bit1 n) ∧
      ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
        ↑d
cases' divMod d n with q r
case bit1.mk
d n : PosNum
q r : Num
IH : ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
      ↑(bit1 n) ∧
    ↑(match (q, r) with
          | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
      ↑d
case bit1.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
        ↑(bit1 n) ∧
      ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
        ↑d
intro IH
case bit1.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(divModAux d q (Num.bit1 r)).snd + ↑d * ↑(divModAux d q (Num.bit1 r)).fst = ↑(bit1 n) ∧
    ↑(divModAux d q (Num.bit1 r)).snd < ↑d
case bit1.mk
d n : PosNum
q r : Num
IH : ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit1 r₁)).fst =
      ↑(bit1 n) ∧
    ↑(match (q, r) with
          | (q, r₁) => divModAux d q (Num.bit1 r₁)).snd <
      ↑d
simp only [divMod] at IH ⊢
case bit1.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r + ↑d * _root_.bit0 ↑q = _root_.bit1 ↑n

case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r < 2 * ↑d
case bit1.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(divModAux d q (Num.bit1 r)).snd + ↑d * ↑(divModAux d q (Num.bit1 r)).fst = ↑(bit1 n) ∧
    ↑(divModAux d q (Num.bit1 r)).snd < ↑d
apply divMod_to_nat_aux <;> simp
no goals
case bit1.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r + ↑d * _root_.bit0 ↑q = _root_.bit1 ↑n
rw [_root_.bit1, _root_.bit1, add_right_comm, bit0_eq_two_mul (n : ℕ), ← IH.1, mul_add, ←
  bit0_eq_two_mul, mul_left_comm, ← bit0_eq_two_mul]
case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r < _root_.bit0 ↑d
case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r < 2 * ↑d
rw [← bit0_eq_two_mul]
no goals
case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit1 ↑r < _root_.bit0 ↑d
exact Nat.bit1_lt_bit0 IH.2
case bit0
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
        ↑d *
          ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
      ↑(bit0 n) ∧
    ↑(match divMod d n with
          | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
      ↑d
case bit0
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(divMod d (bit0 n)).snd + ↑d * ↑(divMod d (bit0 n)).fst = ↑(bit0 n) ∧ ↑(divMod d (bit0 n)).snd < ↑d
unfold divMod
case bit0
d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d →
    ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
          ↑d *
            ↑(match divMod d n with
                | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
        ↑(bit0 n) ∧
      ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
        ↑d
case bit0
d n : PosNum
IH : ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d
⊢ ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
        ↑d *
          ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
      ↑(bit0 n) ∧
    ↑(match divMod d n with
          | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
      ↑d
revert IH
case bit0.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
        ↑(bit0 n) ∧
      ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
        ↑d
case bit0
d n : PosNum
⊢ ↑(divMod d n).snd + ↑d * ↑(divMod d n).fst = ↑n ∧ ↑(divMod d n).snd < ↑d →
    ↑(match divMod d n with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
          ↑d *
            ↑(match divMod d n with
                | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
        ↑(bit0 n) ∧
      ↑(match divMod d n with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
        ↑d
cases' divMod d n with q r
case bit0.mk
d n : PosNum
q r : Num
IH : ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
      ↑(bit0 n) ∧
    ↑(match (q, r) with
          | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
      ↑d
case bit0.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
        ↑(bit0 n) ∧
      ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
        ↑d
intro IH
case bit0.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(divModAux d q (Num.bit0 r)).snd + ↑d * ↑(divModAux d q (Num.bit0 r)).fst = ↑(bit0 n) ∧
    ↑(divModAux d q (Num.bit0 r)).snd < ↑d
case bit0.mk
d n : PosNum
q r : Num
IH : ↑(q, r).snd + ↑d * ↑(q, r).fst = ↑n ∧ ↑(q, r).snd < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => divModAux d q (Num.bit0 r₁)).fst =
      ↑(bit0 n) ∧
    ↑(match (q, r) with
          | (q, r₁) => divModAux d q (Num.bit0 r₁)).snd <
      ↑d
simp only [divMod] at IH ⊢
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r + ↑d * _root_.bit0 ↑q = _root_.bit0 ↑n

case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r < 2 * ↑d
case bit0.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(divModAux d q (Num.bit0 r)).snd + ↑d * ↑(divModAux d q (Num.bit0 r)).fst = ↑(bit0 n) ∧
    ↑(divModAux d q (Num.bit0 r)).snd < ↑d
apply divMod_to_nat_aux <;> simp
no goals
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r + ↑d * _root_.bit0 ↑q = _root_.bit0 ↑n
rw [bit0_eq_two_mul (n : ℕ), ← IH.1, mul_add, ← bit0_eq_two_mul, mul_left_comm, ←
  bit0_eq_two_mul]
case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r < _root_.bit0 ↑d
case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r < 2 * ↑d
rw [← bit0_eq_two_mul]
no goals
case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ _root_.bit0 ↑r < _root_.bit0 ↑d
exact Nat.bit0_lt IH.2