proposition: Lemma afold_right_implb_true_aux : forall a, (exists i, i <? length a - 1 = true /\ a.[i] = false) -> afold_right bool true implb a = true.
proof: Proof. intros a [ i [ Hi Hai ] ]. assert (Bi := to_Z_bounded i). generalize (leb_0 i); apply afold_right_ind. reflexivity. intros _; revert Hi; rewrite ltb_spec, leb_spec; lia. intros b j. assert (Bj := to_Z_bounded j). rewrite ltb_spec, to_Z_0; intro Hj1. rewrite ltb_spec; intro Hj2. rewrite leb_spec; intro IH. rewrite leb_spec, to_Z_sub_1_0 by lia; intro Hji. case (reflect_eqb i (j - 1)). intro Heq; rewrite Heq in Hai; rewrite Hai; reflexivity. rewrite <- to_Z_eq, to_Z_sub_1_0 by lia; intro Hneq. rewrite IH by lia; case (a.[j - 1]); reflexivity. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz