proposition: Lemma Exercise4_6d h: E46_hprop h <-> forall r Z, r <=c (m -c h) -> sub Z (domain X) -> cardinal Z = r +c h -> exists T, [/\ sub T (domain Y), cardinal T = r & forall j, inc j T -> exists2 i, inc i Z & gle E46_order_r i j].
proof: Proof. move: Exercise4_6a Xpr => [[oR sR] rR] [fgX _ _ _]. split; move=> aux r Z pa pb pc; move: (aux _ _ pa pb pc) => [T [tdY cT aux1]]; exists T;split => // j jT. move: (aux1 _ jT) => [k] /setI2_P [kVg] /setUb_P [y]. rewrite restr_d // => yd; rewrite restr_ev//. have yX: inc y (domain X) by apply: pb. have jY: inc j (domain Y) by apply: tdY. move=> kV1; ex_tac; apply/rR;rewrite /E46_u; split;fprops. by right; split => //;exists k; apply: setI2_i. move: (aux1 _ jT) => [i iZ]; move / rR => [_ _ ]. case => h0. empty_tac1 j;rewrite -h0; fprops. move: h0 => [_ _ [k]] /setI2_P [k1 k2]; exists k; apply /setI2_P;split => //. apply /setUb_P; exists i; rewrite ?restr_d //; rewrite restr_ev//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)