no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
⊢ Nodup (replicate 0 a) ↔ 0 ≤ 1
simp [Nat.zero_le]
no goals
α : Type u
β : Type v
l l₁ l₂ : List α
r : α → α → Prop
a✝ b a : α
⊢ Nodup (replicate 1 a) ↔ 1 ≤ 1
simp