proposition: Lemma afold_left_andb_true_inv : forall a, afold_left bool true andb a = true -> forall i, i <? length a = true -> a.[i] = true.
proof: Proof. intros a H i; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i). revert H; rewrite afold_left_spec by apply andb_true_l; apply foldi_ind. apply leb_0. rewrite ltb_spec, to_Z_0; lia. intros j b _; assert (Bj := to_Z_bounded j). rewrite 2!ltb_spec; intros Hj IH. rewrite ltb_spec, to_Z_add_1_wB by lia. rewrite andb_true_iff. case (reflect_eqb i j). intro Heq; rewrite <- Heq; tauto. rewrite <- to_Z_eq; intros Hneq [ Hb Haj ] Hij. apply IH; [ exact Hb | lia ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz