proposition: Lemma card_option : #|{: option T}| = #|T|.+1.
proof: Proof. by rewrite !cardT !enumT [in LHS]unlock /= !size_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)