proposition: Theorem Domino_covers_Black : Surjective _ _ Domino.
proof: Proof. apply Surjections_right with (f := BW). apply (Finite_Board (BW o Domino)). apply Injections_compose. exact BW_One_one. exact Domino_one_one. Qed.
imports: Functions