proposition: Lemma cast_bseq_trans m n p (eq_mn : m = n) (eq_np : n = p) bs : cast_bseq (etrans eq_mn eq_np) bs = cast_bseq eq_np (cast_bseq eq_mn bs).
proof: Proof. by case: n / eq_mn eq_np; case: p /. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)