proposition: Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
proof: Proof. destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl. rewrite Nat2Pos.id by done; simpl. destruct (list_find _ xs) as [[i y]|] eqn:HE; simpl. - apply list_find_Some in HE as (?&?&?); eauto using lookup_lt_Some. - destruct xs; simpl; [|lia]. exfalso; eapply not_elem_of_nil, (HA x). Qed.
imports: stdpp(options)