sorted_divisorsAntidiagonalList_snd

English

The list n.divisorsAntidiagonalList is sorted by the second component in decreasing order.

Русский

Список n.divisorsAntidiagonalList отсортирован по второй компоненте в порядке убывания.

LaTeX

$$$\mathrm{DivisorsAntidiagonalList}(n)\ \text{Sorted by } (\cdot .\mathrm{snd})$ with the relation >.$$

Lean4

theorem sorted_divisorsAntidiagonalList_snd {n : ℕ} : n.divisorsAntidiagonalList.Sorted (·.snd > ·.snd) :=
  by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  refine (List.sorted_lt_range' _ _ Nat.one_ne_zero).filterMap ?_
  simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt, and_imp, Prod.forall, Prod.mk.injEq]
  rintro a b _ _ _ _ ha rfl rfl hb rfl rfl hab
  rwa [Nat.div_lt_div_left hn ⟨_, hb.symm⟩ ⟨_, ha.symm⟩]

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