proposition: Lemma afold_left_andb_false_inv : forall a, afold_left bool true andb a = false -> exists i, (i <? length a = true) /\ (a .[ i] = false).
proof: Proof. intro a; assert (Ba := to_Z_bounded (length a)). rewrite afold_left_spec by apply andb_true_l; apply foldi_ind. apply leb_0. discriminate. intros i b _; assert (Bi := to_Z_bounded i). rewrite ltb_spec; intros Hj IH. destruct b. rewrite andb_true_l; intro H; exists i; rewrite H. split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | reflexivity ]. generalize (IH eq_refl); clear IH; intros [ j [ Hji Haj ] ] _. rewrite ltb_spec in Hji; exists j. split; [ rewrite ltb_spec, to_Z_add_1_wB; lia | exact Haj ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz