proposition: Lemma encode_decode A `{finA: Finite A} i : i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
proof: Proof. destruct finA as [xs Hxs HA]. unfold encode_nat, decode_nat, encode, decode, card; simpl. intros Hi. apply lookup_lt_is_Some in Hi. destruct Hi as [x Hx]. exists x. rewrite !Nat2Pos.id by done; simpl. destruct (list_find_elem_of (x =.) xs x) as [[j y] Hj]; auto. split; [done|]; rewrite Hj; simpl. apply list_find_Some in Hj as (?&->&?). eauto using NoDup_lookup. Qed.
imports: stdpp(options)