proposition: Lemma afold_right_implb_false : forall a, 0 <? length a = true /\ (forall i, i <? length a - 1 = true -> a .[ i] = true) /\ a.[length a - 1] = false -> afold_right bool true implb a = false.
proof: Proof. intros a; intros [H1 [H2 H3]]. pattern 0; apply afold_right_ind. intro H; rewrite H in H1; discriminate. intros _; exact H3. intros b i H4 H5 H6; rewrite H6; clear H6. rewrite H2; [ reflexivity | ]. assert (Ba := to_Z_bounded (length a)); assert (Bi := to_Z_bounded i). revert H1 H4 H5; rewrite 4!ltb_spec, to_Z_0; intros H1 H4 H5. rewrite 2!to_Z_sub_1_0; lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz