proposition: Lemma fin_disj_fam_prop2 A: fin_disj_fam A -> znat_fam (fin_disj_fam_card A).
proof: Proof. rewrite /fin_disj_fam_card; move =>[qa qb qc qd]; saw; fprops. move => i; aw => iz; rewrite (LgV iz); apply card_finite_setP. apply:qd; ue. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)