|apply (inj_times_r (pred ((n-x)!)));
rewrite < (S_pred ((n-x)!))
[rewrite < assoc_times;rewrite < sym_times in \vdash (? ? (? % ?) ?);
- rewrite < H3;generalize in match H2;elim x
+ rewrite < H3;generalize in match H2; elim x
[rewrite < minus_n_O;simplify;rewrite < times_n_SO;reflexivity
|rewrite < fact_minus in H4;
[rewrite > true_to_pi_p_Sn