proposition: Lemma last_belast_eq (T : Type) (x : T) p q : last x p = last x q -> belast x p = belast x q -> p = q.
proof: Proof. elim/last_ind : p => [|p a _]; elim/last_ind : q => [|q b _] //=; try by rewrite belast_rcons => ?. rewrite !belast_rcons !last_rcons => ?. congruence. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)