proposition: Lemma card_sub : #|sfT| = #|[pred x | P x]|.
proof: Proof. by rewrite -(eq_card (codom_val sfT)) (card_image val_inj). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)