proposition: Lemma all_nthP a s x0 : reflect (forall i, i < size s -> a (nth x0 s i)) (all a s).
proof: Proof. rewrite -(eq_all (fun x => negbK (a x))) all_predC. case: (has_nthP _ _ x0) => [na_s | a_s]; [right=> a_s | left=> i lti]. by case: na_s => i lti; rewrite a_s. by apply/idPn=> na_si; case: a_s; exists i. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)