proposition: Lemma Exercise4_6f h: natp h -> E46_hprop h -> exists k, [/\ natp k, k <=c h & order_width E46_order_r (n +c k)].
proof: Proof. move=> hN hp. set r := E46_order_r. have hyp1: (forall x, inc x (free_subsets r) -> (cardinal x) <=c (n +c h)). by move=> t ts;apply: Exercise4_6e. have [x xf cx]:(exists2 x, inc x(free_subsets E46_order_r) & (cardinal x = n)). move: Exercise4_6a => [[oR sR] rR]. exists (domain Y). apply /free_subsetsP; split; first by rewrite sR /E46_u; apply: subsetU2r. move=> x y; rewrite rR; move=> xY yY [_ _ ]; case => //; move=> [xX _]. empty_tac1 x. by move: Ypr => [_ pa _]. have nef: nonempty (free_subsets r) by ex_tac. move: (the_max_card_on_set_prop (NS_sum nN hN) nef hyp1). set k := the_max_card_on_set _; move => [[qa qb] kN]. move: (qb _ xf); rewrite cx => lexk. move: (NS_diff n kN)(cdiff_pr lexk). move => kcN aux; exists (k -c n); split => //; last by rewrite aux. move: qa => [y ys yx]; move: (hyp1 _ ys); rewrite yx -{1} aux. move=> aux3; apply: (csum_le2l nN) => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)