proposition: Lemma nth_image T' y0 (f : T -> T') A (i : 'I_#|A|) : nth y0 (image f A) i = f (enum_val i).
proof: Proof. by rewrite -(nth_map _ y0) // -cardE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)