proposition: Lemma afold_left_orb_true : forall i a, i <? length a = true -> a .[ i] = true -> afold_left bool false orb a = true.
proof: Proof. intros i a; assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i). rewrite afold_left_spec by apply orb_false_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; intro Hij. case (reflect_eqb i j). intros Heq Hai; rewrite <- Heq, Hai; apply orb_true_r. rewrite <- to_Z_eq; intros Hneq Hai. rewrite IH; [ apply orb_true_l | lia | exact Hai ]. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz