proposition: Lemma result_f_LNP_dec_next_minimal_property: forall m p (Hm:le m n_bound) (d : Digit), (m<=p)%nat -> (p< fst (f_LNP_dec_next m Hm))%nat -> ~ P p d.
proof: Proof. intros m p Hm d Hp1 Hp2. assert (Hnbound:=le_not_lt _ _ (result_f_LNP_le_bound m Hm)). functional induction (f_LNP_dec_next m Hm); simpl. intros _; apply Hnbound; apply le_lt_trans with p; trivial; rewrite <- _x; assumption... intros _; simpl in Hp2; apply (lt_irrefl m); apply le_lt_trans with p; assumption... intros _; simpl in Hp2; apply (lt_irrefl m); apply le_lt_trans with p; assumption... intros _; simpl in Hp2; apply (lt_irrefl m); apply le_lt_trans with p; assumption... destruct (le_lt_eq_dec _ _ Hp1) as [Hp3|Hp3]. assert (Hp4:=lt_le_S _ _ Hp3); apply (IHp0 Hp4 Hp2 Hnbound). rewrite <- Hp3; destruct d; assumption. Qed.
imports: Recdef digits