proposition: Lemma map_size_ne_0_lookup {A} (m : M A) : size m ≠ 0 ↔ ∃ i, is_Some (m !! i).
proof: Proof. rewrite map_size_non_empty_iff. split. - intros Hsz. apply map_choose. intros Hemp. done. - intros [i [k Hi]] ->. rewrite lookup_empty in Hi. done. Qed.
imports: Coq(Permutation) stdpp(options)