proposition: Lemma LNP_sigS_nat_Digit: {n:nat& {d:Digit | P n d/\ forall m d, (lt m n) -> ~(P m d)}}.
proof: Proof. remember f_LNP_dec_all as nd. exists (fst nd); exists (snd nd); split. subst nd; apply result_f_LNP_dec_all_has_property... intros m d Hm; subst nd; apply result_f_LNP_dec_all_minimal_property; assumption... Qed.
imports: Recdef digits