proposition: Lemma index_find x l a : has a l -> index (nth x l (find a l)) l = find a l.
proof: Proof. move=> Hal. apply/eqP; rewrite eqn_leq leq_index_nth. case: leqP => // /(before_find x). by rewrite nth_index ?nth_find // mem_nth // -has_find. Qed.
imports: mathcomp(all_ssreflect) extra