apply (nat_elim2 (\lambda n,n2.
((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to
apply (nat_elim2 (\lambda n,n2.
((nth_prime i) \sup n)*(defactorize_aux n1 (S i)) =
((nth_prime i) \sup n2)*(defactorize_aux n3 (S i)) \to