proposition: Lemma upath_size x y p : upath x y p -> size p < #|D|.
proof: Proof. move=> /upath_uniq/card_uniqP/= <-. exact: max_card. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)