proposition: Lemma eqvb_transL (X : elabelType) b b' (u u' v : X) : u' ≡[b (+) b'] v -> u ≡[b'] u' -> u ≡[b] v.
proof: Proof. move => A B. move:(eqvb_trans B A). by rewrite addbC -addbA addbb addbF. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)