proposition: Lemma injective_prepend (T : finType) (lmax : nat) (c : seq T) : injective (@prepend T lmax c).
proof: Proof. move=> /= a b [] /eqP. rewrite eqseq_cat // => /andP[_ /eqP ab]; by apply val_inj. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext