proposition: Lemma extension_perm n s (es := extension s n n): natp n -> inc s (permutations n) -> [/\ inc es (permutations (csucc n)), Vf es n = n & forall i, inc i n -> Vf es i = Vf s i].
proof: Proof. move => nN /permutationsP [bs ss ts]. have Ha: ~ inc n (source s) by rewrite ss; apply:(Nat_decent nN). have Hb: ~ inc n (target s) by rewrite ts -{2} ss. split. - apply/permutationsP; split. + exact:(extension_fb Ha Hb bs). + by rewrite /es /extension; aw; rewrite ss (succ_of_nat nN). + by rewrite /es /extension; aw; rewrite ts (succ_of_nat nN). - by rewrite (extension_Vf_out n (proj1 (proj1 bs)) Ha). - rewrite - ss;move => i lin. by rewrite (extension_Vf_in n (proj1 (proj1 bs)) Ha). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)