proposition: Lemma partition_fam_partition f x: partition_s_fam f x -> partition_s (range f) x.
proof: Proof. move=> [pf hyp]; move: (partition_same2 pf)=> [ur di]. move:pf=> [fgf md _]; split=>//. move=> a /(rangeP (proj1 fgf)) [b bf]; move: (pr2_V fgf bf); aw => ->. apply: hyp;ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)