proposition: Lemma last_take (T : eqType) (x : T) (p : seq T) (n : nat): n <= size p -> last x (take n p) = nth x (x :: p) n.
proof: Proof. elim: p x n => [|a p IHp] x [|n] Hn //=. by rewrite IHp // (set_nth_default a x). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)