proposition: Lemma fin_disj_fam_enum_range_p1 A x: fin_disj_fam A -> inc x (unionb A) -> inc (fin_disj_fam_enum A x) (fin_disj_fam_enum_range A).
proof: Proof. move => ha hb. move: (proj32(proj1 (fin_disj_fam_prop3 ha hb))) => h; apply: (Zo_i h). by (exists x). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)