Documentation

Mathlib.Data.Num.Lemmas

Properties of the binary representation of integers #

@[simp]
theorem PosNum.cast_one {α : Type u_1} [One α] [Add α] :
1 = 1
@[simp]
theorem PosNum.cast_one' {α : Type u_1} [One α] [Add α] :
@[simp]
theorem PosNum.cast_bit0 {α : Type u_1} [One α] [Add α] (n : PosNum) :
n.bit0 = n + n
@[simp]
theorem PosNum.cast_bit1 {α : Type u_1} [One α] [Add α] (n : PosNum) :
n.bit1 = n + n + 1
@[simp]
theorem PosNum.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) :
n = n
theorem PosNum.to_nat_to_int (n : PosNum) :
n = n
@[simp]
theorem PosNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : PosNum) :
n = n
theorem PosNum.succ_to_nat (n : PosNum) :
n.succ = n + 1
theorem PosNum.one_add (n : PosNum) :
1 + n = n.succ
theorem PosNum.add_one (n : PosNum) :
n + 1 = n.succ
theorem PosNum.add_to_nat (m : PosNum) (n : PosNum) :
(m + n) = m + n
theorem PosNum.add_succ (m : PosNum) (n : PosNum) :
m + n.succ = (m + n).succ
theorem PosNum.bit0_of_bit0 (n : PosNum) :
n + n = n.bit0
theorem PosNum.bit1_of_bit1 (n : PosNum) :
n + n + 1 = n.bit1
theorem PosNum.mul_to_nat (m : PosNum) (n : PosNum) :
(m * n) = m * n
theorem PosNum.to_nat_pos (n : PosNum) :
0 < n
theorem PosNum.cmp_to_nat_lemma {m : PosNum} {n : PosNum} :
m < nm.bit1 < n.bit0
theorem PosNum.cmp_swap (m : PosNum) (n : PosNum) :
(m.cmp n).swap = n.cmp m
theorem PosNum.cmp_to_nat (m : PosNum) (n : PosNum) :
Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
theorem PosNum.lt_to_nat {m : PosNum} {n : PosNum} :
m < n m < n
theorem PosNum.le_to_nat {m : PosNum} {n : PosNum} :
m n m n
theorem Num.add_zero (n : Num) :
n + 0 = n
theorem Num.zero_add (n : Num) :
0 + n = n
theorem Num.add_one (n : Num) :
n + 1 = n.succ
theorem Num.add_succ (m : Num) (n : Num) :
m + n.succ = (m + n).succ
theorem Num.bit0_of_bit0 (n : Num) :
n + n = n.bit0
theorem Num.bit1_of_bit1 (n : Num) :
n + n + 1 = n.bit1
@[simp]
theorem Num.ofNat'_bit (b : Bool) (n : ) :
Num.ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (Num.ofNat' n)
@[simp]
theorem Num.bit1_succ (n : Num) :
n.bit1.succ = n.succ.bit0
@[simp]
theorem Num.add_ofNat' (m : ) (n : ) :
@[simp]
theorem Num.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] :
0 = 0
@[simp]
theorem Num.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] :
Num.zero = 0
@[simp]
theorem Num.cast_one {α : Type u_1} [Zero α] [One α] [Add α] :
1 = 1
@[simp]
theorem Num.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] (n : PosNum) :
(Num.pos n) = n
theorem Num.succ'_to_nat (n : Num) :
n.succ' = n + 1
theorem Num.succ_to_nat (n : Num) :
n.succ = n + 1
@[simp]
theorem Num.cast_to_nat {α : Type u_1} [AddMonoidWithOne α] (n : Num) :
n = n
theorem Num.add_to_nat (m : Num) (n : Num) :
(m + n) = m + n
theorem Num.mul_to_nat (m : Num) (n : Num) :
(m * n) = m * n
theorem Num.cmp_to_nat (m : Num) (n : Num) :
Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
theorem Num.lt_to_nat {m : Num} {n : Num} :
m < n m < n
theorem Num.le_to_nat {m : Num} {n : Num} :
m n m n
@[simp]
@[simp]
theorem Num.of_to_nat' (n : Num) :
Num.ofNat' n = n
theorem Num.to_nat_inj {m : Num} {n : Num} :
m = n m = n

This tactic tries to turn an (in)equality about Nums to one about Nats by rewriting.

example (n : Num) (m : Num) : n ≤ n + m := by
  transfer_rw
  exact Nat.le_add_right _ _
Equations
Instances For

    This tactic tries to prove (in)equalities about Nums by transferring them to the Nat world and then trying to call simp.

    example (n : Num) (m : Num) : n ≤ n + m := by transfer
    
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      theorem Num.add_of_nat (m : ) (n : ) :
      (m + n) = m + n
      theorem Num.to_nat_to_int (n : Num) :
      n = n
      @[simp]
      theorem Num.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : Num) :
      n = n
      theorem Num.to_of_nat (n : ) :
      n = n
      @[simp]
      theorem Num.of_natCast {α : Type u_1} [AddMonoidWithOne α] (n : ) :
      n = n
      @[deprecated Num.of_natCast]
      theorem Num.of_nat_cast {α : Type u_1} [AddMonoidWithOne α] (n : ) :
      n = n

      Alias of Num.of_natCast.

      theorem Num.of_nat_inj {m : } {n : } :
      m = n m = n
      @[simp]
      theorem Num.of_to_nat (n : Num) :
      n = n
      theorem Num.dvd_to_nat (m : Num) (n : Num) :
      m n m n
      @[simp]
      theorem PosNum.of_to_nat (n : PosNum) :
      n = Num.pos n
      theorem PosNum.to_nat_inj {m : PosNum} {n : PosNum} :
      m = n m = n
      theorem PosNum.pred'_to_nat (n : PosNum) :
      n.pred' = (↑n).pred
      @[simp]
      theorem PosNum.pred'_succ' (n : Num) :
      n.succ'.pred' = n
      @[simp]
      theorem PosNum.succ'_pred' (n : PosNum) :
      n.pred'.succ' = n
      Equations
      theorem PosNum.dvd_to_nat {m : PosNum} {n : PosNum} :
      m n m n
      theorem PosNum.size_to_nat (n : PosNum) :
      n.size = (↑n).size
      theorem PosNum.size_eq_natSize (n : PosNum) :
      n.size = n.natSize
      theorem PosNum.natSize_to_nat (n : PosNum) :
      n.natSize = (↑n).size
      theorem PosNum.natSize_pos (n : PosNum) :
      0 < n.natSize

      This tactic tries to turn an (in)equality about PosNums to one about Nats by rewriting.

      example (n : PosNum) (m : PosNum) : n ≤ n + m := by
        transfer_rw
        exact Nat.le_add_right _ _
      
      Equations
      Instances For

        This tactic tries to prove (in)equalities about PosNums by transferring them to the Nat world and then trying to call simp.

        example (n : PosNum) (m : PosNum) : n ≤ n + m := by transfer
        
        Equations
        Instances For
          @[simp]
          theorem PosNum.cast_to_num (n : PosNum) :
          n = Num.pos n
          @[simp]
          theorem PosNum.bit_to_nat (b : Bool) (n : PosNum) :
          (PosNum.bit b n) = Nat.bit b n
          @[simp]
          theorem PosNum.cast_add {α : Type u_1} [AddMonoidWithOne α] (m : PosNum) (n : PosNum) :
          (m + n) = m + n
          @[simp]
          theorem PosNum.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : PosNum) :
          n.succ = n + 1
          @[simp]
          theorem PosNum.cast_inj {α : Type u_1} [AddMonoidWithOne α] [CharZero α] {m : PosNum} {n : PosNum} :
          m = n m = n
          @[simp]
          theorem PosNum.one_le_cast {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) :
          1 n
          @[simp]
          theorem PosNum.cast_pos {α : Type u_1} [LinearOrderedSemiring α] (n : PosNum) :
          0 < n
          @[simp]
          theorem PosNum.cast_mul {α : Type u_1} [Semiring α] (m : PosNum) (n : PosNum) :
          (m * n) = m * n
          @[simp]
          theorem PosNum.cmp_eq (m : PosNum) (n : PosNum) :
          m.cmp n = Ordering.eq m = n
          @[simp]
          theorem PosNum.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : PosNum} {n : PosNum} :
          m < n m < n
          @[simp]
          theorem PosNum.cast_le {α : Type u_1} [LinearOrderedSemiring α] {m : PosNum} {n : PosNum} :
          m n m n
          theorem Num.bit_to_nat (b : Bool) (n : Num) :
          (Num.bit b n) = Nat.bit b n
          theorem Num.cast_succ' {α : Type u_1} [AddMonoidWithOne α] (n : Num) :
          n.succ' = n + 1
          theorem Num.cast_succ {α : Type u_1} [AddMonoidWithOne α] (n : Num) :
          n.succ = n + 1
          @[simp]
          theorem Num.cast_add {α : Type u_1} [Semiring α] (m : Num) (n : Num) :
          (m + n) = m + n
          @[simp]
          theorem Num.cast_bit0 {α : Type u_1} [Semiring α] (n : Num) :
          n.bit0 = 2 * n
          @[simp]
          theorem Num.cast_bit1 {α : Type u_1} [Semiring α] (n : Num) :
          n.bit1 = 2 * n + 1
          @[simp]
          theorem Num.cast_mul {α : Type u_1} [Semiring α] (m : Num) (n : Num) :
          (m * n) = m * n
          theorem Num.size_to_nat (n : Num) :
          n.size = (↑n).size
          theorem Num.size_eq_natSize (n : Num) :
          n.size = n.natSize
          theorem Num.natSize_to_nat (n : Num) :
          n.natSize = (↑n).size
          @[simp]
          theorem Num.ofNat'_eq (n : ) :
          Num.ofNat' n = n
          theorem Num.zneg_toZNum (n : Num) :
          -n.toZNum = n.toZNumNeg
          theorem Num.zneg_toZNumNeg (n : Num) :
          -n.toZNumNeg = n.toZNum
          theorem Num.toZNum_inj {m : Num} {n : Num} :
          m.toZNum = n.toZNum m = n
          @[simp]
          theorem Num.cast_toZNum {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : Num) :
          n.toZNum = n
          @[simp]
          theorem Num.cast_toZNumNeg {α : Type u_1} [AddGroup α] [One α] (n : Num) :
          n.toZNumNeg = -n
          @[simp]
          theorem Num.add_toZNum (m : Num) (n : Num) :
          (m + n).toZNum = m.toZNum + n.toZNum
          theorem PosNum.pred_to_nat {n : PosNum} (h : 1 < n) :
          n.pred = (↑n).pred
          theorem PosNum.sub'_one (a : PosNum) :
          a.sub' 1 = a.pred'.toZNum
          theorem PosNum.one_sub' (a : PosNum) :
          PosNum.sub' 1 a = a.pred'.toZNumNeg
          theorem PosNum.lt_iff_cmp {m : PosNum} {n : PosNum} :
          m < n m.cmp n = Ordering.lt
          theorem PosNum.le_iff_cmp {m : PosNum} {n : PosNum} :
          m n m.cmp n Ordering.gt
          theorem Num.pred_to_nat (n : Num) :
          n.pred = (↑n).pred
          theorem Num.ppred_to_nat (n : Num) :
          castNum <$> n.ppred = (↑n).ppred
          theorem Num.cmp_swap (m : Num) (n : Num) :
          (m.cmp n).swap = n.cmp m
          theorem Num.cmp_eq (m : Num) (n : Num) :
          m.cmp n = Ordering.eq m = n
          @[simp]
          theorem Num.cast_lt {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m < n m < n
          @[simp]
          theorem Num.cast_le {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m n m n
          @[simp]
          theorem Num.cast_inj {α : Type u_1} [LinearOrderedSemiring α] {m : Num} {n : Num} :
          m = n m = n
          theorem Num.lt_iff_cmp {m : Num} {n : Num} :
          m < n m.cmp n = Ordering.lt
          theorem Num.le_iff_cmp {m : Num} {n : Num} :
          m n m.cmp n Ordering.gt
          theorem Num.castNum_eq_bitwise {f : NumNumNum} {g : BoolBoolBool} (p : PosNumPosNumNum) (gff : g false false = false) (f00 : f 0 0 = 0) (f0n : ∀ (n : PosNum), f 0 (Num.pos n) = bif g false true then Num.pos n else 0) (fn0 : ∀ (n : PosNum), f (Num.pos n) 0 = bif g true false then Num.pos n else 0) (fnn : ∀ (m n : PosNum), f (Num.pos m) (Num.pos n) = p m n) (p11 : p 1 1 = bif g true true then 1 else 0) (p1b : ∀ (b : Bool) (n : PosNum), p 1 (PosNum.bit b n) = Num.bit (g true b) (bif g false true then Num.pos n else 0)) (pb1 : ∀ (a : Bool) (m : PosNum), p (PosNum.bit a m) 1 = Num.bit (g a true) (bif g true false then Num.pos m else 0)) (pbb : ∀ (a b : Bool) (m n : PosNum), p (PosNum.bit a m) (PosNum.bit b n) = Num.bit (g a b) (p m n)) (m : Num) (n : Num) :
          (f m n) = Nat.bitwise g m n
          @[simp]
          theorem Num.castNum_or (m : Num) (n : Num) :
          (m ||| n) = m ||| n
          @[simp]
          theorem Num.castNum_and (m : Num) (n : Num) :
          (m &&& n) = m &&& n
          @[simp]
          theorem Num.castNum_ldiff (m : Num) (n : Num) :
          (m.ldiff n) = (↑m).ldiff n
          @[simp]
          theorem Num.castNum_xor (m : Num) (n : Num) :
          (m ^^^ n) = m ^^^ n
          @[simp]
          theorem Num.castNum_shiftLeft (m : Num) (n : ) :
          (m <<< n) = m <<< n
          @[simp]
          theorem Num.castNum_shiftRight (m : Num) (n : ) :
          (m >>> n) = m >>> n
          @[simp]
          theorem Num.castNum_testBit (m : Num) (n : ) :
          m.testBit n = (↑m).testBit n
          @[simp]
          theorem ZNum.cast_zero {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
          0 = 0
          @[simp]
          theorem ZNum.cast_zero' {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
          @[simp]
          theorem ZNum.cast_one {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] :
          1 = 1
          @[simp]
          theorem ZNum.cast_pos {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) :
          (ZNum.pos n) = n
          @[simp]
          theorem ZNum.cast_neg {α : Type u_1} [Zero α] [One α] [Add α] [Neg α] (n : PosNum) :
          (ZNum.neg n) = -n
          @[simp]
          theorem ZNum.cast_zneg {α : Type u_1} [AddGroup α] [One α] (n : ZNum) :
          (-n) = -n
          theorem ZNum.neg_zero :
          -0 = 0
          theorem ZNum.zneg_zneg (n : ZNum) :
          - -n = n
          theorem ZNum.zneg_bit1 (n : ZNum) :
          -n.bit1 = (-n).bitm1
          theorem ZNum.zneg_bitm1 (n : ZNum) :
          -n.bitm1 = (-n).bit1
          theorem ZNum.zneg_succ (n : ZNum) :
          -n.succ = (-n).pred
          theorem ZNum.zneg_pred (n : ZNum) :
          -n.pred = (-n).succ
          @[simp]
          theorem ZNum.abs_to_nat (n : ZNum) :
          n.abs = (↑n).natAbs
          @[simp]
          theorem ZNum.abs_toZNum (n : Num) :
          n.toZNum.abs = n
          @[simp]
          theorem ZNum.cast_to_int {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n = n
          theorem ZNum.bit0_of_bit0 (n : ZNum) :
          n + n = n.bit0
          theorem ZNum.bit1_of_bit1 (n : ZNum) :
          n + n + 1 = n.bit1
          @[simp]
          theorem ZNum.cast_bit0 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n.bit0 = n + n
          @[simp]
          theorem ZNum.cast_bit1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n.bit1 = n + n + 1
          @[simp]
          theorem ZNum.cast_bitm1 {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n.bitm1 = n + n - 1
          theorem ZNum.add_zero (n : ZNum) :
          n + 0 = n
          theorem ZNum.zero_add (n : ZNum) :
          0 + n = n
          theorem ZNum.add_one (n : ZNum) :
          n + 1 = n.succ
          theorem PosNum.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : PosNum) (n : PosNum) :
          (m.sub' n) = m - n
          theorem PosNum.to_nat_eq_succ_pred (n : PosNum) :
          n = n.pred' + 1
          theorem PosNum.to_int_eq_succ_pred (n : PosNum) :
          n = n.pred' + 1
          @[simp]
          theorem Num.cast_sub' {α : Type u_1} [AddGroupWithOne α] (m : Num) (n : Num) :
          (m.sub' n) = m - n
          theorem Num.toZNum_succ (n : Num) :
          n.succ.toZNum = n.toZNum.succ
          theorem Num.toZNumNeg_succ (n : Num) :
          n.succ.toZNumNeg = n.toZNumNeg.pred
          @[simp]
          theorem Num.pred_succ (n : ZNum) :
          n.pred.succ = n
          theorem Num.ofInt'_toZNum (n : ) :
          (↑n).toZNum = ZNum.ofInt' n
          theorem Num.mem_ofZNum' {m : Num} {n : ZNum} :
          m Num.ofZNum' n n = m.toZNum
          theorem Num.ofZNum'_toNat (n : ZNum) :
          castNum <$> Num.ofZNum' n = (↑n).toNat'
          @[simp]
          theorem Num.ofZNum_toNat (n : ZNum) :
          (Num.ofZNum n) = (↑n).toNat
          @[simp]
          theorem Num.cast_ofZNum {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          (Num.ofZNum n) = (↑n).toNat
          @[simp]
          theorem Num.sub_to_nat (m : Num) (n : Num) :
          (m - n) = m - n
          @[simp]
          theorem ZNum.cast_add {α : Type u_1} [AddGroupWithOne α] (m : ZNum) (n : ZNum) :
          (m + n) = m + n
          @[simp]
          theorem ZNum.cast_succ {α : Type u_1} [AddGroupWithOne α] (n : ZNum) :
          n.succ = n + 1
          @[simp]
          theorem ZNum.mul_to_int (m : ZNum) (n : ZNum) :
          (m * n) = m * n
          theorem ZNum.cast_mul {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) :
          (m * n) = m * n
          theorem ZNum.of_to_int' (n : ZNum) :
          ZNum.ofInt' n = n
          theorem ZNum.to_int_inj {m : ZNum} {n : ZNum} :
          m = n m = n
          theorem ZNum.cmp_to_int (m : ZNum) (n : ZNum) :
          Ordering.casesOn (m.cmp n) (m < n) (m = n) (n < m)
          theorem ZNum.lt_to_int {m : ZNum} {n : ZNum} :
          m < n m < n
          theorem ZNum.le_to_int {m : ZNum} {n : ZNum} :
          m n m n
          @[simp]
          theorem ZNum.cast_lt {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} :
          m < n m < n
          @[simp]
          theorem ZNum.cast_le {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} :
          m n m n
          @[simp]
          theorem ZNum.cast_inj {α : Type u_1} [LinearOrderedRing α] {m : ZNum} {n : ZNum} :
          m = n m = n

          This tactic tries to turn an (in)equality about ZNums to one about Ints by rewriting.

          example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
            transfer_rw
            exact le_add_of_nonneg_right (mul_self_nonneg _)
          
          Equations
          Instances For

            This tactic tries to prove (in)equalities about ZNums by transferring them to the Int world and then trying to call simp.

            example (n : ZNum) (m : ZNum) : n ≤ n + m * m := by
              transfer
              exact mul_self_nonneg _
            
            Equations
            Instances For
              @[simp]
              theorem ZNum.cast_sub {α : Type u_1} [Ring α] (m : ZNum) (n : ZNum) :
              (m - n) = m - n
              theorem ZNum.neg_of_int (n : ) :
              (-n) = -n
              @[simp]
              theorem ZNum.ofInt'_eq (n : ) :
              ZNum.ofInt' n = n
              @[simp]
              theorem ZNum.of_nat_toZNum (n : ) :
              (↑n).toZNum = n
              @[simp]
              theorem ZNum.of_to_int (n : ZNum) :
              n = n
              theorem ZNum.to_of_int (n : ) :
              n = n
              @[simp]
              theorem ZNum.of_nat_toZNumNeg (n : ) :
              (↑n).toZNumNeg = -n
              @[simp]
              theorem ZNum.of_intCast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n
              @[deprecated ZNum.of_intCast]
              theorem ZNum.of_int_cast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n

              Alias of ZNum.of_intCast.

              @[simp]
              theorem ZNum.of_natCast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n
              @[deprecated ZNum.of_natCast]
              theorem ZNum.of_nat_cast {α : Type u_1} [AddGroupWithOne α] (n : ) :
              n = n

              Alias of ZNum.of_natCast.

              @[simp]
              theorem ZNum.dvd_to_int (m : ZNum) (n : ZNum) :
              m n m n
              theorem PosNum.divMod_to_nat_aux {n : PosNum} {d : PosNum} {q : Num} {r : Num} (h₁ : r + d * (q + q) = n) (h₂ : r < 2 * d) :
              (d.divModAux q r).2 + d * (d.divModAux q r).1 = n (d.divModAux q r).2 < d
              theorem PosNum.divMod_to_nat (d : PosNum) (n : PosNum) :
              n / d = (d.divMod n).1 n % d = (d.divMod n).2
              @[simp]
              theorem PosNum.div'_to_nat (n : PosNum) (d : PosNum) :
              (n.div' d) = n / d
              @[simp]
              theorem PosNum.mod'_to_nat (n : PosNum) (d : PosNum) :
              (n.mod' d) = n % d
              @[simp]
              theorem Num.div_zero (n : Num) :
              n / 0 = 0
              @[simp]
              theorem Num.div_to_nat (n : Num) (d : Num) :
              (n / d) = n / d
              @[simp]
              theorem Num.mod_zero (n : Num) :
              n % 0 = n
              @[simp]
              theorem Num.mod_to_nat (n : Num) (d : Num) :
              (n % d) = n % d
              theorem Num.gcd_to_nat_aux {n : } {a : Num} {b : Num} :
              a b(a * b).natSize n(Num.gcdAux n a b) = (↑a).gcd b
              @[simp]
              theorem Num.gcd_to_nat (a : Num) (b : Num) :
              (a.gcd b) = (↑a).gcd b
              theorem Num.dvd_iff_mod_eq_zero {m : Num} {n : Num} :
              m n n % m = 0
              instance Num.decidableDvd :
              DecidableRel fun (x1 x2 : Num) => x1 x2
              Equations
              instance PosNum.decidableDvd :
              DecidableRel fun (x1 x2 : PosNum) => x1 x2
              Equations
              @[simp]
              theorem ZNum.div_zero (n : ZNum) :
              n / 0 = 0
              @[simp]
              theorem ZNum.div_to_int (n : ZNum) (d : ZNum) :
              (n / d) = n / d
              @[simp]
              theorem ZNum.mod_to_int (n : ZNum) (d : ZNum) :
              (n % d) = n % d
              @[simp]
              theorem ZNum.gcd_to_nat (a : ZNum) (b : ZNum) :
              (a.gcd b) = (↑a).gcd b
              theorem ZNum.dvd_iff_mod_eq_zero {m : ZNum} {n : ZNum} :
              m n n % m = 0
              instance ZNum.decidableDvd :
              DecidableRel fun (x1 x2 : ZNum) => x1 x2
              Equations

              Cast a SNum to the corresponding integer.

              Equations
              Instances For
                Equations
                instance SNum.lt :
                Equations
                instance SNum.le :
                Equations