proposition: Lemma eqvb_trans (X : elabelType) (u v w : X) (b1 b2 : bool) : u ≡[b1] v -> v ≡[b2] w -> u ≡[b1 (+) b2] w.
proof: Proof. case: b1; case: b2 => /=; try solve [exact: eqv01|exact: eqv11|exact: eqv10]. by transitivity v. Qed.
imports: HB(structures) Coq(RelationClasses Morphisms Relation_Definitions) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop bij)