proposition: Lemma deg_Knm n m (x : 'K_n,m) : minn n m <= #|N(x)|.
proof: Proof. by case: x => [x|y]; rewrite ?deg_Knm_l ?deg_Knm_r ?geq_minr ?geq_minl. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)