apply divides_max_p_defactorize.
qed.
lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
\lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
intros.
apply divides_max_p_defactorize.
qed.
lemma not_eq_nf_cons_O_nf_cons: \forall f,g:nat_fact.\forall n,i:nat.
\lnot (defactorize_aux (nf_cons O f) i= defactorize_aux (nf_cons (S n) g) i).
intros.