proposition: Lemma add_stack_nwf x e : x \in white e -> wf_color e -> wf_num e -> wf_num (add_stack x e).
proof: Proof. move=> x_w wf_c wf_e. have [nEw nEc nLs snE pE] := wf_e. split => [y|y|y||y z]; rewrite ?ffunE ?inE /=. - rewrite white_add_stack; case: (y =P x) => [->|/eqP yDx]; rewrite !inE. by rewrite snE eqxx. by rewrite nEw (negPf yDx). - case: (y =P x) => [->|//]. rewrite eqn_leq snE [#|V|.+1 <= _]leqNgt !ltnS. rewrite -(cardsC (gray e :|: black e)) (@cardsD1 _ x (~: _)) !inE. case: color4P x_w => //= x_w. by rewrite addnS ltnS leq_addr andbF. - by case: (y == x) => // nE; rewrite ltnS ltnW // nLs. - rewrite gray_add_stack // snE. rewrite [in RHS](cardD1 x) !inE eqxx /=; congr (_.+2). apply: eq_card => z; rewrite !inE. by case: (z =P x) => //= ->; case: color4P x_w. - rewrite ![_ == x]eq_sym. do 2 case: eqP => //=. * by rewrite leqnn. * by rewrite leqNgt num_stackP => // _ _ _ /andP[_ ->]. * by rewrite num_stackP => // _ _ /andP[_ nLs1]; rewrite ltnW. * by move=> *; apply: pE. Qed.
imports: mathcomp(all_ssreflect) bigmin extra