proposition: Lemma Exercise5_9l1 n q p (E:= Nint (q *c n)): natp n -> natp q -> \0c <c q -> inc p (partition_nq E q) -> Ex59_compl n q (Ex59_splitA q p) = union (Ex59_splitB q p).
proof: Proof. move => nN qN qp /Zo_P [/partitionsP [[ha hb] hc] hd]. rewrite/Ex59_compl /Ex59_splitB /Ex59_splitA'. set J := (Ex59_splitA q p). set iv := (fun j : Set => Nintcc j (j +c (q -c \1c))). rewrite -/E - ha. set_extens t. move/setC_P => [/setU_P [z sa zb]] zc; apply /setU_P; exists z => //. apply/setC_P; split => // /funI_P [v vj zv]; case: zc; union_tac. apply/funI_P; ex_tac. move/setU_P => [z za /setC_P [zb zc]]; apply/setC_P; split; first union_tac. move/setU_P => [v va /funI_P[j jj jv]]; case: zc. move:(Exercise5_9j3 qN qp jj). rewrite -/(iv _) - jv; move => [jN jp]. apply/funI_P; ex_tac; rewrite - jv. by case:(hb _ _ zb jp) => // di; empty_tac1 t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)