proposition: Lemma Exercise5_9j5 E n q p k: natp n -> natp q -> \0c <c q -> cardinal E = q *c n -> inc p (Ex59_k_interval E q k) -> cardinal (Ex59_splitA q p) = k /\ cardinal (Ex59_splitA' q p) = k.
proof: Proof. move => nN qN qp cE /Zo_P [pq pb]. set T:= (Ex59_splitA q p). pose W:= (Exercise5_9j2 qN qp). suff ct: cardinal T = k. split; [ exact | rewrite - ct; apply:cardinal_fun_image]. move => a b /funI_P [z /Zo_hi zv ->]. by move /funI_P => [z' /Zo_hi zv' ->]; rewrite - (W _ zv) - (W _ zv') => ->. rewrite -pb; apply:cardinal_fun_image. move => i j /Zo_P [ha hb]/Zo_P [hc hd] ee. by rewrite (W _ hb) (W _ hd) ee. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)