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