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