proposition: Lemma afold_right_implb_true : forall a, length a = 0 \/ (exists i, i <? length a - 1 = true /\ a.[i] = false) \/ (forall i, i <? length a = true -> a.[i] = true) -> afold_right bool true implb a = true.
proof: Proof. intro a; assert (Ba := to_Z_bounded (length a)); case (reflect_eqb (length a) 0). intros H _; unfold afold_right; rewrite H; reflexivity. intro Hneq. intros [H1|[H1|H1]]. elim (Hneq H1). apply afold_right_implb_true_aux; auto. assert (Heq : length a =? 0 = false) by (rewrite <- not_true_iff_false, eqb_spec; exact Hneq). unfold afold_right; rewrite Heq. revert Hneq; rewrite <- to_Z_eq, to_Z_0; intro Hneq. apply (foldi_ind _ (fun i a => a = true)). rewrite leb_spec, to_Z_1; lia. apply H1; rewrite ltb_spec, to_Z_sub_1_0; lia. intros i b; assert (Bi := to_Z_bounded i). rewrite leb_spec, to_Z_1; intro Hi1. rewrite ltb_spec; intros Hi2 IH. rewrite IH; case (a.[length a - 1 - i]); reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz