unitInterval.qRight.proof_1

theorem unitInterval.qRight.proof_1 : 0 ≤ 1

This theorem, named `unitInterval.qRight.proof_1`, states that zero is less than or equal to one. This is a fundamental concept in number comparisons and it holds true in the context of all real numbers. The Lean 4 proof for this theorem is not provided here.

More concisely: The theorem `unitInterval.qRight.proof_1` asserts that 0 ≤ 1 in the context of real numbers.