proposition: Lemma result_f_LNP_dec_all_minimal_property: forall (p : nat) (d : Digit), (p < fst f_LNP_dec_all)%nat -> ~ P p d.
proof: Proof. unfold f_LNP_dec_all. intros p d Hp. apply (result_f_LNP_dec_next_minimal_property O) with (le_O_n n_bound); trivial; apply le_O_n. Qed.
imports: Recdef digits