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