proposition: Lemma forall_n_correct : forall n, forall_n n = true -> forall p, p <= n -> P p = true.
proof: Proof. induction n ; simpl. - intros. assert (p = 0) by lia. congruence. - intros. rewrite andb_true_iff in H. destruct H. specialize (IHn H1 p). assert (p = S n \/ p <= n) by lia. destruct H2 ; subst; auto. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR