proposition: Lemma Knm_connected n m : connected [set: 'K_n.+1,m.+1].
proof: Proof. apply: (@connected_center _ (inl ord0 : 'K_n.+1,m.+1)) => // y _. rewrite restrictE; last by move=> ?; rewrite inE. case: y => [y|y]; last exact: connect1. by apply: (@connect_trans _ _ (inr ord0)); apply: connect1. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)