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