proposition: Lemma leq_card_in A : {in A &, injective f} -> #|A| <= #|T'|.
proof: Proof. by move=> /card_in_image <-; rewrite max_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)