Mathlib.Data.Nat.ChineseRemainder._auxLemma.1

theorem Mathlib.Data.Nat.ChineseRemainder._auxLemma.1 : ∀ {a b : ℕ}, (a ≡ b [MOD 1]) = True

This theorem states that for any two natural numbers 'a' and 'b', the equivalence of 'a' and 'b' modulo 1 is always true. In mathematical terms, it means that 'a' and 'b' leave the same remainder when divided by 1, which is always true because any number divided by 1 leaves no remainder.

More concisely: For all natural numbers a and b, a = b mod 1.