proposition: Lemma result_f_LNP_dec_next_has_property:forall m (Hm:le m n_bound), let (n,d):=f_LNP_dec_next m Hm in P n d.
proof: Proof. intros m Hm. remember (f_LNP_dec_next m Hm) as nd; destruct nd. functional induction (f_LNP_dec_next m Hm); [ | | | |apply IHp; assumption]; assert (H_eq:=f_equal (@fst nat Digit) Heqnd); simpl in H_eq; rewrite H_eq; clear H_eq; assert (H_eq:=f_equal (@snd nat Digit) Heqnd); simpl in H_eq; rewrite H_eq; trivial. exact (proj2_sig n_bound_has_d)... Qed.
imports: Recdef digits