proposition: Theorem Cockayne_Hedetniemi_chain_w: sorted leq [:: ir_w; gamma_w; ii_w; alpha_w; Gamma_w; IR_w].
proof: Proof. rewrite /sorted /= ir_w_leq_gamma_w gamma_w_leq_ii_w ii_w_leq_alpha_w. by rewrite alpha_w_leq_Gamma_w Gamma_w_leq_IR_w. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)