+(* zero - zero *)
+reflexivity.
+(* zero - one *)
+simplify in H1.
+apply False_ind.
+apply not_eq_O_S O H1.
+(* zero - proper *)
+simplify in H1.
+apply False_ind.
+apply not_le_Sn_n O.
+rewrite > H1 in \vdash (? ? %).
+change with O < defactorize_aux n O.
+apply lt_O_defactorize_aux.
+generalize in match H.
+elim g.
+(* one - zero *)
+simplify in H1.
+apply False_ind.
+apply not_eq_O_S O.apply sym_eq. assumption.
+(* one - one *)
+reflexivity.
+(* one - proper *)
+simplify in H1.
+apply False_ind.
+apply not_le_Sn_n (S O).
+rewrite > H1 in \vdash (? ? %).
+change with (S O) < defactorize_aux n O.
+apply lt_SO_defactorize_aux.
+generalize in match H.elim g.
+(* proper - zero *)
+simplify in H1.
+apply False_ind.
+apply not_le_Sn_n O.
+rewrite < H1 in \vdash (? ? %).
+change with O < defactorize_aux n O.
+apply lt_O_defactorize_aux.
+(* proper - one *)
+simplify in H1.
+apply False_ind.
+apply not_le_Sn_n (S O).
+rewrite < H1 in \vdash (? ? %).
+change with (S O) < defactorize_aux n O.
+apply lt_SO_defactorize_aux.
+(* proper - proper *)
+apply eq_f.
+apply injective_defactorize_aux O.
+exact H1.
+qed.
+
+theorem factorize_defactorize:
+\forall f,g: nat_fact_all. factorize (defactorize f) = f.
+intros.
+apply injective_defactorize.
+(* uffa: perche' semplifica ??? *)
+change with defactorize(factorize (defactorize f)) = (defactorize f).
+apply defactorize_factorize.
+qed.