proposition: Lemma partition_same2 y x: partition_w_fam y x -> partition_w (range y) x.
proof: Proof. move=> [fg md uyx]; split; first by rewrite - setUb_alt. move=> a b /(range_gP fg) [u ud ->] /(range_gP fg) [v vd ->]. by case: (md _ _ ud vd) ;[ move=>->|]; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)