← Copula mathematical handbook

Homomorphism rules for USize used by the grind tactic. The injection function is USize.toBitVec.

theorem Lean.Grind.USize.toNat_eq_toBitVec_toNat (x : USize) : x.toNat = x.toBitVec.toNat

Translations of ≤ and < into the target domain.