theorem pos_num.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

theorem pos_num.cast_one' {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

theorem pos_num.cast_bit0 {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : pos_num) :

theorem pos_num.cast_bit1 {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : pos_num) :

theorem pos_num.cast_to_nat {α : Type u_1} [add_monoid α] [has_one α] (n : pos_num) :

theorem pos_num.to_nat_to_int (n : pos_num) :

theorem pos_num.cast_to_int {α : Type u_1} [add_group α] [has_one α] (n : pos_num) :

theorem pos_num.succ_to_nat (n : pos_num) :

theorem pos_num.one_add (n : pos_num) :

theorem pos_num.add_one (n : pos_num) :

theorem pos_num.add_to_nat (m n : pos_num) :

theorem pos_num.add_succ (m n : pos_num) :

theorem pos_num.bit0_of_bit0 (n : pos_num) :

theorem pos_num.bit1_of_bit1 (n : pos_num) :

theorem pos_num.mul_to_nat (m n : pos_num) :

theorem pos_num.to_nat_pos (n : pos_num) :

theorem pos_num.cmp_to_nat_lemma {m n : pos_num} (a : ↑m < ↑n) :

theorem pos_num.cmp_swap (m n : pos_num) :

theorem pos_num.cmp_to_nat (m n : pos_num) :

theorem pos_num.lt_to_nat {m n : pos_num} :

theorem pos_num.le_to_nat {m n : pos_num} :

theorem num.add_zero (n : num) :

theorem num.zero_add (n : num) :

theorem num.add_one (n : num) :

theorem num.add_succ (m n : num) :

theorem num.add_of_nat (m n : ℕ) :

theorem num.bit0_of_bit0 (n : num) :

theorem num.bit1_of_bit1 (n : num) :

theorem num.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

theorem num.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

theorem num.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] :

theorem num.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] (n : pos_num) :

theorem num.succ'_to_nat (n : num) :

theorem num.succ_to_nat (n : num) :

theorem num.cast_to_nat {α : Type u_1} [add_monoid α] [has_one α] (n : num) :

theorem num.to_nat_to_int (n : num) :

theorem num.cast_to_int {α : Type u_1} [add_group α] [has_one α] (n : num) :

theorem num.to_of_nat (n : ℕ) :

theorem num.of_nat_cast {α : Type u_1} [add_monoid α] [has_one α] (n : ℕ) :

theorem num.of_nat_inj {m n : ℕ} :

theorem num.add_to_nat (m n : num) :

theorem num.mul_to_nat (m n : num) :

theorem num.cmp_to_nat (m n : num) :

theorem num.lt_to_nat {m n : num} :

theorem num.le_to_nat {m n : num} :

theorem pos_num.of_to_nat (n : pos_num) :

theorem num.of_to_nat (n : num) :

theorem num.to_nat_inj {m n : num} :

theorem num.dvd_to_nat (m n : num) :

theorem pos_num.to_nat_inj {m n : pos_num} :

theorem pos_num.pred'_to_nat (n : pos_num) :

theorem pos_num.pred'_succ' (n : num) :

theorem pos_num.succ'_pred' (n : pos_num) :

theorem pos_num.dvd_to_nat {m n : pos_num} :

theorem pos_num.size_to_nat (n : pos_num) :

theorem pos_num.size_eq_nat_size (n : pos_num) :

theorem pos_num.nat_size_to_nat (n : pos_num) :

theorem pos_num.nat_size_pos (n : pos_num) :

theorem pos_num.cast_to_num (n : pos_num) :

theorem pos_num.bit_to_nat (b : bool) (n : pos_num) :

theorem pos_num.cast_add {α : Type u_1} [add_monoid α] [has_one α] (m n : pos_num) :

theorem pos_num.cast_succ {α : Type u_1} [add_monoid α] [has_one α] (n : pos_num) :

theorem pos_num.cast_inj {α : Type u_1} [add_monoid α] [has_one α] [char_zero α] {m n : pos_num} :

theorem pos_num.one_le_cast {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :

theorem pos_num.cast_pos {α : Type u_1} [linear_ordered_semiring α] (n : pos_num) :

theorem pos_num.cast_mul {α : Type u_1} [semiring α] (m n : pos_num) :

theorem pos_num.cmp_eq (m n : pos_num) :

theorem pos_num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :

theorem pos_num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : pos_num} :

theorem num.bit_to_nat (b : bool) (n : num) :

theorem num.cast_succ' {α : Type u_1} [add_monoid α] [has_one α] (n : num) :

theorem num.cast_succ {α : Type u_1} [add_monoid α] [has_one α] (n : num) :

theorem num.cast_add {α : Type u_1} [semiring α] (m n : num) :

theorem num.cast_bit0 {α : Type u_1} [semiring α] (n : num) :

theorem num.cast_bit1 {α : Type u_1} [semiring α] (n : num) :

theorem num.cast_mul {α : Type u_1} [semiring α] (m n : num) :

theorem num.size_to_nat (n : num) :

theorem num.size_eq_nat_size (n : num) :

theorem num.nat_size_to_nat (n : num) :

theorem num.of_nat'_eq (n : ℕ) :

theorem num.zneg_to_znum (n : num) :

theorem num.zneg_to_znum_neg (n : num) :

theorem num.to_znum_inj {m n : num} :

theorem num.cast_to_znum {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : num) :

theorem num.cast_to_znum_neg {α : Type u_1} [add_group α] [has_one α] (n : num) :

theorem num.add_to_znum (m n : num) :

theorem pos_num.pred_to_nat {n : pos_num} (h : 1 < n) :

theorem pos_num.sub'_one (a : pos_num) :

theorem pos_num.one_sub' (a : pos_num) :

theorem pos_num.lt_iff_cmp {m n : pos_num} :

theorem pos_num.le_iff_cmp {m n : pos_num} :

theorem num.pred_to_nat (n : num) :

theorem num.ppred_to_nat (n : num) :

theorem num.cmp_swap (m n : num) :

theorem num.cmp_eq (m n : num) :

theorem num.cast_lt {α : Type u_1} [linear_ordered_semiring α] {m n : num} :

theorem num.cast_le {α : Type u_1} [linear_ordered_semiring α] {m n : num} :

theorem num.cast_inj {α : Type u_1} [linear_ordered_semiring α] {m n : num} :

theorem num.lt_iff_cmp {m n : num} :

theorem num.le_iff_cmp {m n : num} :

theorem num.bitwise_to_nat {f : num → num → num} {g : bool → bool → bool} (p : pos_num → pos_num → num) (gff : g ff ff = ff) (f00 : f 0 0 = 0) (f0n : ∀ (n : pos_num), f 0 (num.pos n) = cond (g ff tt) (num.pos n) 0) (fn0 : ∀ (n : pos_num), f (num.pos n) 0 = cond (g tt ff) (num.pos n) 0) (fnn : ∀ (m n : pos_num), f (num.pos m) (num.pos n) = p m n) (p11 : p 1 1 = cond (g tt tt) 1 0) (p1b : ∀ (b : bool) (n : pos_num), p 1 (pos_num.bit b n) = num.bit (g tt b) (cond (g ff tt) (num.pos n) 0)) (pb1 : ∀ (a : bool) (m : pos_num), p (pos_num.bit a m) 1 = num.bit (g a tt) (cond (g tt ff) (num.pos m) 0)) (pbb : ∀ (a b : bool) (m n : pos_num), p (pos_num.bit a m) (pos_num.bit b n) = num.bit (g a b) (p m n)) (m n : num) :

theorem num.lor_to_nat (m n : num) :

theorem num.land_to_nat (m n : num) :

theorem num.ldiff_to_nat (m n : num) :

theorem num.lxor_to_nat (m n : num) :

theorem num.shiftl_to_nat (m : num) (n : ℕ) :

theorem num.shiftr_to_nat (m : num) (n : ℕ) :

theorem num.test_bit_to_nat (m : num) (n : ℕ) :

theorem znum.cast_zero {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

theorem znum.cast_zero' {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

theorem znum.cast_one {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] :

theorem znum.cast_pos {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :

theorem znum.cast_neg {α : Type u_1} [has_zero α] [has_one α] [has_add α] [has_neg α] (n : pos_num) :

theorem znum.cast_zneg {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.neg_zero  :

theorem znum.zneg_pos (n : pos_num) :

theorem znum.zneg_neg (n : pos_num) :

theorem znum.zneg_zneg (n : znum) :

theorem znum.zneg_bit1 (n : znum) :

theorem znum.zneg_bitm1 (n : znum) :

theorem znum.zneg_succ (n : znum) :

theorem znum.zneg_pred (n : znum) :

theorem znum.neg_of_int (n : ℤ) :

theorem znum.abs_to_nat (n : znum) :

theorem znum.abs_to_znum (n : num) :

theorem znum.cast_to_int {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.bit0_of_bit0 (n : znum) :

theorem znum.bit1_of_bit1 (n : znum) :

theorem znum.cast_bit0 {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.cast_bit1 {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.cast_bitm1 {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.add_zero (n : znum) :

theorem znum.zero_add (n : znum) :

theorem znum.add_one (n : znum) :

theorem pos_num.cast_to_znum (n : pos_num) :

theorem pos_num.cast_sub' {α : Type u_1} [add_group α] [has_one α] (m n : pos_num) :

theorem pos_num.to_nat_eq_succ_pred (n : pos_num) :

theorem pos_num.to_int_eq_succ_pred (n : pos_num) :

theorem num.cast_sub' {α : Type u_1} [add_group α] [has_one α] (m n : num) :

theorem num.of_nat_to_znum (n : ℕ) :

theorem num.of_nat_to_znum_neg (n : ℕ) :

theorem num.mem_of_znum' {m : num} {n : znum} :

theorem num.of_znum'_to_nat (n : znum) :

theorem num.of_znum_to_nat (n : znum) :

theorem num.cast_of_znum {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem num.sub_to_nat (m n : num) :

theorem znum.cast_add {α : Type u_1} [add_group α] [has_one α] (m n : znum) :

theorem znum.cast_succ {α : Type u_1} [add_group α] [has_one α] (n : znum) :

theorem znum.mul_to_int (m n : znum) :

theorem znum.cast_mul {α : Type u_1} [ring α] (m n : znum) :

theorem znum.of_to_int (n : znum) :

theorem znum.to_of_int (n : ℤ) :

theorem znum.to_int_inj {m n : znum} :

theorem znum.of_int_cast {α : Type u_1} [add_group α] [has_one α] (n : ℤ) :

theorem znum.of_nat_cast {α : Type u_1} [add_group α] [has_one α] (n : ℕ) :

theorem znum.of_int'_eq (n : ℤ) :

theorem znum.cmp_to_int (m n : znum) :

theorem znum.lt_to_int {m n : znum} :

theorem znum.le_to_int {m n : znum} :

theorem znum.cast_lt {α : Type u_1} [linear_ordered_ring α] {m n : znum} :

theorem znum.cast_le {α : Type u_1} [linear_ordered_ring α] {m n : znum} :

theorem znum.cast_inj {α : Type u_1} [linear_ordered_ring α] {m n : znum} :

theorem znum.dvd_to_int (m n : znum) :

theorem pos_num.divmod_to_nat_aux {n d : pos_num} {q r : num} (h₁ : ↑r + (↑d) * bit0 ↑q = ↑n) (h₂ : ↑r < 2 * ↑d) :

theorem pos_num.divmod_to_nat (d n : pos_num) :

theorem pos_num.div'_to_nat (n d : pos_num) :

theorem pos_num.mod'_to_nat (n d : pos_num) :

theorem num.div_to_nat (n d : num) :

theorem num.mod_to_nat (n d : num) :

theorem num.gcd_to_nat_aux {n : ℕ} {a b : num} (a_1 : a ≤ b) (a_2 : (a * b).nat_size ≤ n) :

theorem num.gcd_to_nat (a b : num) :

theorem num.dvd_iff_mod_eq_zero {m n : num} :

theorem znum.div_to_int (n d : znum) :

theorem znum.mod_to_int (n d : znum) :

theorem znum.gcd_to_nat (a b : znum) :

theorem znum.dvd_iff_mod_eq_zero {m n : znum} :