proposition: Lemma derangeS1 n (p := n.+1 * derange n): derange n.+1 = if (odd n) then p.+1 else p.-1.
proof: Proof. have pa: forall s, 0 <derange s.+2. elim => // s dp; rewrite derangeS muln_gt0 ltn0Sn addn_gt0 dp orbT //. have pn: forall s, ~~odd s -> 0 < (s.+1) * derange s. by case => //;case => // s _; rewrite muln_gt0 ltn0Sn pa. rewrite /p {p};elim :n => // n Hrec; rewrite derangeS Hrec /=. move: (pn n); case (odd n). move => _; rewrite /negb (mulSnr n.+1) [in X in _ = X] addnS succnK. by rewrite - mulnDr (addnC). by move => /= h; rewrite mulnDr; rewrite -{1} (@prednK (n.+1 * _)) // h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)