Documentation

Init.Data.UInt.Lemmas

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem UInt8.le_trans {a : UInt8} {b : UInt8} {c : UInt8} :
    a bb ca c
    theorem UInt8.one_def :
    1 = { val := 1 }
    theorem UInt8.lt_trans {a : UInt8} {b : UInt8} {c : UInt8} :
    a < bb < ca < c
    @[simp]
    theorem UInt8.not_lt {a : UInt8} {b : UInt8} :
    ¬a < b b a
    theorem UInt8.mod_def (a : UInt8) (b : UInt8) :
    a % b = { val := a.val % b.val }
    theorem UInt8.zero_def :
    0 = { val := 0 }
    @[simp]
    theorem UInt8.mk_val_eq (a : UInt8) :
    { val := a.val } = a
    theorem UInt8.add_def (a : UInt8) (b : UInt8) :
    a + b = { val := a.val + b.val }
    theorem UInt8.sub_def (a : UInt8) (b : UInt8) :
    a - b = { val := a.val - b.val }
    theorem UInt8.val_eq_of_eq {a : UInt8} {b : UInt8} (h : a = b) :
    a.val = b.val
    theorem UInt8.ne_of_val_ne {a : UInt8} {b : UInt8} (h : a.val b.val) :
    a b
    theorem UInt8.mul_def (a : UInt8) (b : UInt8) :
    a * b = { val := a.val * b.val }
    theorem UInt8.ne_of_lt {a : UInt8} {b : UInt8} (h : a < b) :
    a b
    theorem UInt8.mod_lt (a : UInt8) (b : UInt8) (h : 0 < b) :
    a % b < b
    theorem UInt8.modn_lt {m : Nat} (u : UInt8) :
    m > 0(u % m).toNat < m
    @[simp]
    theorem UInt8.modn_toNat (a : UInt8) (b : Nat) :
    (a.modn b).toNat = a.toNat % b
    theorem UInt8.le_total (a : UInt8) (b : UInt8) :
    a b b a
    @[simp]
    theorem UInt8.lt_irrefl (a : UInt8) :
    ¬a < a
    @[simp]
    @[simp]
    theorem UInt8.div_toNat (a : UInt8) (b : UInt8) :
    (a / b).toNat = a.toNat / b.toNat
    @[simp]
    theorem UInt8.le_refl (a : UInt8) :
    a a
    @[simp]
    theorem UInt8.not_le {a : UInt8} {b : UInt8} :
    ¬a b b < a
    theorem UInt8.val_eq_of_lt {a : Nat} :
    a < UInt8.size(UInt8.ofNat a).val = a
    @[simp]
    theorem UInt8.mod_toNat (a : UInt8) (b : UInt8) :
    (a % b).toNat = a.toNat % b.toNat
    theorem UInt8.lt_iff_val_lt_val {a : UInt8} {b : UInt8} :
    a < b a.val < b.val
    theorem UInt8.lt_asymm {a : UInt8} {b : UInt8} (h : a < b) :
    ¬b < a
    theorem UInt8.eq_of_val_eq {a : UInt8} {b : UInt8} (h : a.val = b.val) :
    a = b
    theorem UInt8.toNat.inj {a : UInt8} {b : UInt8} :
    a.toNat = b.toNata = b
    theorem UInt8.le_def {a : UInt8} {b : UInt8} :
    a b a.val b.val
    theorem UInt8.lt_def {a : UInt8} {b : UInt8} :
    a < b a.val < b.val
    theorem UInt16.add_def (a : UInt16) (b : UInt16) :
    a + b = { val := a.val + b.val }
    theorem UInt16.le_trans {a : UInt16} {b : UInt16} {c : UInt16} :
    a bb ca c
    theorem UInt16.val_eq_of_eq {a : UInt16} {b : UInt16} (h : a = b) :
    a.val = b.val
    @[simp]
    theorem UInt16.le_refl (a : UInt16) :
    a a
    theorem UInt16.lt_iff_val_lt_val {a : UInt16} {b : UInt16} :
    a < b a.val < b.val
    @[simp]
    theorem UInt16.mk_val_eq (a : UInt16) :
    { val := a.val } = a
    theorem UInt16.le_def {a : UInt16} {b : UInt16} :
    a b a.val b.val
    theorem UInt16.lt_asymm {a : UInt16} {b : UInt16} (h : a < b) :
    ¬b < a
    @[simp]
    theorem UInt16.lt_irrefl (a : UInt16) :
    ¬a < a
    @[simp]
    theorem UInt16.not_lt {a : UInt16} {b : UInt16} :
    ¬a < b b a
    @[simp]
    theorem UInt16.mod_toNat (a : UInt16) (b : UInt16) :
    (a % b).toNat = a.toNat % b.toNat
    theorem UInt16.one_def :
    1 = { val := 1 }
    @[simp]
    theorem UInt16.div_toNat (a : UInt16) (b : UInt16) :
    (a / b).toNat = a.toNat / b.toNat
    theorem UInt16.lt_def {a : UInt16} {b : UInt16} :
    a < b a.val < b.val
    theorem UInt16.zero_def :
    0 = { val := 0 }
    @[simp]
    theorem UInt16.not_le {a : UInt16} {b : UInt16} :
    ¬a b b < a
    @[simp]
    theorem UInt16.modn_toNat (a : UInt16) (b : Nat) :
    (a.modn b).toNat = a.toNat % b
    theorem UInt16.mod_def (a : UInt16) (b : UInt16) :
    a % b = { val := a.val % b.val }
    theorem UInt16.ne_of_lt {a : UInt16} {b : UInt16} (h : a < b) :
    a b
    theorem UInt16.le_total (a : UInt16) (b : UInt16) :
    a b b a
    theorem UInt16.mod_lt (a : UInt16) (b : UInt16) (h : 0 < b) :
    a % b < b
    theorem UInt16.mul_def (a : UInt16) (b : UInt16) :
    a * b = { val := a.val * b.val }
    theorem UInt16.sub_def (a : UInt16) (b : UInt16) :
    a - b = { val := a.val - b.val }
    theorem UInt16.toNat.inj {a : UInt16} {b : UInt16} :
    a.toNat = b.toNata = b
    theorem UInt16.ne_of_val_ne {a : UInt16} {b : UInt16} (h : a.val b.val) :
    a b
    theorem UInt16.val_eq_of_lt {a : Nat} :
    a < UInt16.size(UInt16.ofNat a).val = a
    theorem UInt16.modn_lt {m : Nat} (u : UInt16) :
    m > 0(u % m).toNat < m
    theorem UInt16.eq_of_val_eq {a : UInt16} {b : UInt16} (h : a.val = b.val) :
    a = b
    theorem UInt16.lt_trans {a : UInt16} {b : UInt16} {c : UInt16} :
    a < bb < ca < c
    theorem UInt32.ne_of_lt {a : UInt32} {b : UInt32} (h : a < b) :
    a b
    theorem UInt32.mod_def (a : UInt32) (b : UInt32) :
    a % b = { val := a.val % b.val }
    theorem UInt32.toNat.inj {a : UInt32} {b : UInt32} :
    a.toNat = b.toNata = b
    theorem UInt32.le_def {a : UInt32} {b : UInt32} :
    a b a.val b.val
    theorem UInt32.add_def (a : UInt32) (b : UInt32) :
    a + b = { val := a.val + b.val }
    theorem UInt32.ne_of_val_ne {a : UInt32} {b : UInt32} (h : a.val b.val) :
    a b
    @[simp]
    theorem UInt32.mk_val_eq (a : UInt32) :
    { val := a.val } = a
    theorem UInt32.zero_def :
    0 = { val := 0 }
    @[simp]
    theorem UInt32.div_toNat (a : UInt32) (b : UInt32) :
    (a / b).toNat = a.toNat / b.toNat
    theorem UInt32.lt_iff_val_lt_val {a : UInt32} {b : UInt32} :
    a < b a.val < b.val
    theorem UInt32.modn_lt {m : Nat} (u : UInt32) :
    m > 0(u % m).toNat < m
    theorem UInt32.lt_trans {a : UInt32} {b : UInt32} {c : UInt32} :
    a < bb < ca < c
    theorem UInt32.mul_def (a : UInt32) (b : UInt32) :
    a * b = { val := a.val * b.val }
    theorem UInt32.eq_of_val_eq {a : UInt32} {b : UInt32} (h : a.val = b.val) :
    a = b
    theorem UInt32.val_eq_of_lt {a : Nat} :
    a < UInt32.size(UInt32.ofNat a).val = a
    @[simp]
    theorem UInt32.lt_irrefl (a : UInt32) :
    ¬a < a
    theorem UInt32.lt_asymm {a : UInt32} {b : UInt32} (h : a < b) :
    ¬b < a
    @[simp]
    theorem UInt32.not_le {a : UInt32} {b : UInt32} :
    ¬a b b < a
    theorem UInt32.val_eq_of_eq {a : UInt32} {b : UInt32} (h : a = b) :
    a.val = b.val
    @[simp]
    theorem UInt32.modn_toNat (a : UInt32) (b : Nat) :
    (a.modn b).toNat = a.toNat % b
    theorem UInt32.le_total (a : UInt32) (b : UInt32) :
    a b b a
    theorem UInt32.one_def :
    1 = { val := 1 }
    theorem UInt32.sub_def (a : UInt32) (b : UInt32) :
    a - b = { val := a.val - b.val }
    @[simp]
    theorem UInt32.le_refl (a : UInt32) :
    a a
    theorem UInt32.mod_lt (a : UInt32) (b : UInt32) (h : 0 < b) :
    a % b < b
    theorem UInt32.le_trans {a : UInt32} {b : UInt32} {c : UInt32} :
    a bb ca c
    theorem UInt32.lt_def {a : UInt32} {b : UInt32} :
    a < b a.val < b.val
    @[simp]
    theorem UInt32.not_lt {a : UInt32} {b : UInt32} :
    ¬a < b b a
    @[simp]
    theorem UInt32.mod_toNat (a : UInt32) (b : UInt32) :
    (a % b).toNat = a.toNat % b.toNat
    theorem UInt64.add_def (a : UInt64) (b : UInt64) :
    a + b = { val := a.val + b.val }
    theorem UInt64.mod_def (a : UInt64) (b : UInt64) :
    a % b = { val := a.val % b.val }
    theorem UInt64.val_eq_of_lt {a : Nat} :
    a < UInt64.size(UInt64.ofNat a).val = a
    @[simp]
    theorem UInt64.lt_irrefl (a : UInt64) :
    ¬a < a
    theorem UInt64.zero_def :
    0 = { val := 0 }
    theorem UInt64.lt_asymm {a : UInt64} {b : UInt64} (h : a < b) :
    ¬b < a
    theorem UInt64.le_total (a : UInt64) (b : UInt64) :
    a b b a
    theorem UInt64.val_eq_of_eq {a : UInt64} {b : UInt64} (h : a = b) :
    a.val = b.val
    theorem UInt64.le_trans {a : UInt64} {b : UInt64} {c : UInt64} :
    a bb ca c
    theorem UInt64.lt_def {a : UInt64} {b : UInt64} :
    a < b a.val < b.val
    theorem UInt64.lt_iff_val_lt_val {a : UInt64} {b : UInt64} :
    a < b a.val < b.val
    theorem UInt64.sub_def (a : UInt64) (b : UInt64) :
    a - b = { val := a.val - b.val }
    theorem UInt64.mod_lt (a : UInt64) (b : UInt64) (h : 0 < b) :
    a % b < b
    theorem UInt64.eq_of_val_eq {a : UInt64} {b : UInt64} (h : a.val = b.val) :
    a = b
    @[simp]
    theorem UInt64.mod_toNat (a : UInt64) (b : UInt64) :
    (a % b).toNat = a.toNat % b.toNat
    @[simp]
    theorem UInt64.not_le {a : UInt64} {b : UInt64} :
    ¬a b b < a
    theorem UInt64.mul_def (a : UInt64) (b : UInt64) :
    a * b = { val := a.val * b.val }
    @[simp]
    theorem UInt64.not_lt {a : UInt64} {b : UInt64} :
    ¬a < b b a
    @[simp]
    theorem UInt64.modn_toNat (a : UInt64) (b : Nat) :
    (a.modn b).toNat = a.toNat % b
    theorem UInt64.toNat.inj {a : UInt64} {b : UInt64} :
    a.toNat = b.toNata = b
    @[simp]
    theorem UInt64.div_toNat (a : UInt64) (b : UInt64) :
    (a / b).toNat = a.toNat / b.toNat
    theorem UInt64.lt_trans {a : UInt64} {b : UInt64} {c : UInt64} :
    a < bb < ca < c
    theorem UInt64.modn_lt {m : Nat} (u : UInt64) :
    m > 0(u % m).toNat < m
    theorem UInt64.ne_of_lt {a : UInt64} {b : UInt64} (h : a < b) :
    a b
    @[simp]
    theorem UInt64.mk_val_eq (a : UInt64) :
    { val := a.val } = a
    theorem UInt64.le_def {a : UInt64} {b : UInt64} :
    a b a.val b.val
    theorem UInt64.one_def :
    1 = { val := 1 }
    theorem UInt64.ne_of_val_ne {a : UInt64} {b : UInt64} (h : a.val b.val) :
    a b
    @[simp]
    theorem UInt64.le_refl (a : UInt64) :
    a a
    theorem USize.toNat.inj {a : USize} {b : USize} :
    a.toNat = b.toNata = b
    @[simp]
    theorem USize.mk_val_eq (a : USize) :
    { val := a.val } = a
    theorem USize.val_eq_of_lt {a : Nat} :
    a < USize.size(USize.ofNat a).val = a
    theorem USize.lt_iff_val_lt_val {a : USize} {b : USize} :
    a < b a.val < b.val
    theorem USize.ne_of_val_ne {a : USize} {b : USize} (h : a.val b.val) :
    a b
    theorem USize.mod_lt (a : USize) (b : USize) (h : 0 < b) :
    a % b < b
    @[simp]
    @[simp]
    theorem USize.modn_toNat (a : USize) (b : Nat) :
    (a.modn b).toNat = a.toNat % b
    @[simp]
    theorem USize.div_toNat (a : USize) (b : USize) :
    (a / b).toNat = a.toNat / b.toNat
    theorem USize.lt_asymm {a : USize} {b : USize} (h : a < b) :
    ¬b < a
    @[simp]
    theorem USize.mod_toNat (a : USize) (b : USize) :
    (a % b).toNat = a.toNat % b.toNat
    theorem USize.le_trans {a : USize} {b : USize} {c : USize} :
    a bb ca c
    theorem USize.zero_def :
    0 = { val := 0 }
    theorem USize.modn_lt {m : Nat} (u : USize) :
    m > 0(u % m).toNat < m
    theorem USize.lt_def {a : USize} {b : USize} :
    a < b a.val < b.val
    theorem USize.ne_of_lt {a : USize} {b : USize} (h : a < b) :
    a b
    theorem USize.val_eq_of_eq {a : USize} {b : USize} (h : a = b) :
    a.val = b.val
    theorem USize.sub_def (a : USize) (b : USize) :
    a - b = { val := a.val - b.val }
    @[simp]
    theorem USize.not_lt {a : USize} {b : USize} :
    ¬a < b b a
    theorem USize.le_def {a : USize} {b : USize} :
    a b a.val b.val
    theorem USize.eq_of_val_eq {a : USize} {b : USize} (h : a.val = b.val) :
    a = b
    theorem USize.one_def :
    1 = { val := 1 }
    theorem USize.add_def (a : USize) (b : USize) :
    a + b = { val := a.val + b.val }
    theorem USize.lt_trans {a : USize} {b : USize} {c : USize} :
    a < bb < ca < c
    theorem USize.mul_def (a : USize) (b : USize) :
    a * b = { val := a.val * b.val }
    @[simp]
    theorem USize.le_refl (a : USize) :
    a a
    theorem USize.mod_def (a : USize) (b : USize) :
    a % b = { val := a.val % b.val }
    @[simp]
    theorem USize.lt_irrefl (a : USize) :
    ¬a < a
    @[simp]
    theorem USize.not_le {a : USize} {b : USize} :
    ¬a b b < a
    theorem USize.le_total (a : USize) (b : USize) :
    a b b a