proposition: Lemma boolean_witness_nonzero : forall k p, linear k p -> ~ null p -> eval (boolean_witness p) p = true.
proof: Proof. intros k p Hl Hp; induction Hl; simpl. - destruct c; [reflexivity|elim Hp; now constructor]. - case_decide. + rewrite eval_null_zero; [|assumption]; rewrite list_replace_nth_2; simpl. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. now intros j Hd; apply list_replace_nth_1; lia. + rewrite list_replace_nth_2, xorb_false_r. erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto]. now intros j Hd; apply list_replace_nth_1; lia. Qed.
imports: Bool DecidableClass Algebra Ring PArith Lia