feat(data/fin): pos_iff_nonempty (#8975)

leanprover-community · Sep 6, 2021 · c0f01ee · c0f01ee
1 parent de37a6a
commit c0f01ee
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/data/fin.lean b/src/data/fin.lean
@@ -94,6 +94,9 @@ variables {n m : ℕ} {a b : fin n}
 
 instance fin_to_nat (n : ℕ) : has_coe (fin n) nat := ⟨subtype.val⟩
 
+lemma pos_iff_nonempty {n : ℕ} : 0 < n ↔ nonempty (fin n) :=
+⟨λ h, ⟨⟨0, h⟩⟩, λ ⟨i⟩, lt_of_le_of_lt (nat.zero_le _) i.2⟩
+
 section coe
 
 /-!