proposition: Lemma opn_Knm_r n m (y : 'I_m) : N(inr y : 'K_n,m) = [set inl x | x in [set: 'I_n]].
proof: Proof. apply/setP=> -[z|z]; rewrite ?mem_imset ?inE //; first exact: inl_inj. by symmetry; apply: contraTF isT => /imsetP [z']. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)