proposition: Lemma bforall_lt_aux_ok : forall n b, bforall_lt_aux b n = true <-> b = true /\ forall_lt n.
proof: Proof. unfold forall_lt. induction n; simpl; intros. bool. firstorder auto with zarith. rewrite andb_eq, IHn, bP_ok. intuition. destruct (Nat.eq_dec i n). subst. hyp. apply H2. lia. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil)