proposition: Corollary Cockayne_Hedetniemi_chain: sorted leq [:: ir; gamma; ii; alpha; Gamma; IR].
proof: Proof. rewrite /sorted /= ir_leq_gamma gamma_leq_ii ii_leq_alpha. by rewrite alpha_leq_Gamma Gamma_leq_IR. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)