cmp_swap — Mathlib

English

For any m, (cmp m n).swap = cmp n m.

Русский

Для любых m выполняется, что (cmp m n).swap = cmp n m.

LaTeX

$$$ (\\mathrm{cmp}\, m\\, n).\\mathrm{swap} = \\mathrm{cmp}\\, n\\, m $$$

Lean4

theorem cmp_swap (m) : ∀ n, (cmp m n).swap = cmp n m := by
  induction m with
                | one => ?_
                | bit1 m IH => ?_
                | bit0 m IH => ?_ <;>
                intro n <;>
              obtain - | n | n := n <;>
            unfold cmp <;>
          try { rfl
          } <;>
        rw [← IH] <;>
      cases cmp m n <;>
    rfl

Похожие утверждения