proposition: Lemma pickle_Knn_inj : injective pickle_Knm.
proof: Proof. case => -[i Hi]; case => -[j Hj] => //= Eij. - congr (inl _); exact/val_inj. - case:notF. by rewrite Eij -ltn_subRL subnn ltn0 in Hi. - case:notF. by rewrite -Eij -ltn_subRL subnn ltn0 in Hj. - congr (inr _). by apply/val_inj/eqP; rewrite /= -(eqn_add2l n) Eij. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)