Theorem: HTPI.nondec_cons (HTPILib/Chap7.lean)

State before:
n : ℕ
L : List ℕ
⊢ nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L
Tactic:
rfl
State after:
no goals