proposition: Lemma ffactnSr (n : int) (m : nat) : n ^_ m.+1 = n ^_ m * (n - Posz m).
proof: Proof. elim : m n => [ | m Hm] n. by rewrite ffactn1 ffactn0 mul1r subr0. rewrite ffactnS Hm ffactnS -mulrA; repeat congr (_ * _). by rewrite -!addrA; congr(_ + _); rewrite -addn1 -oppzD addrC. Qed.
imports: mathcomp(all_ssreflect all_algebra) tactics