proposition: Lemma tuto_option_enumP : forall T : finType, Finite.axiom (option_enum T).
proof: Proof. by move=> T; case=> [x|]; rewrite /= count_map (count_pred0, enumP). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)