proposition: Lemma transposition_prop n i j (f:=Lf (fun z => variant i j (variant j i z z) z) n n): natp n -> inc i n -> inc j n -> [/\ inc f (permutations n), Vf f i = j, Vf f j = i, forall k, inc k n -> k <> i -> k <> j -> (Vf f k) = k & forall k, inc k n -> Vf f (Vf f k) = k].
proof: Proof. move => nN iE jE. have ax: lf_axiom (fun z => variant i j (variant j i z z) z) n n. rewrite /variant => z; Ytac h1; [ ue | Ytac h2; [ ue | done]]. have pa: Vf f i = j by rewrite /f LfV // variant_true0. have pb: Vf f j = i by rewrite /f/variant LfV//; Ytac h1 => //; Ytac0. have pc: forall k, inc k n -> k <> i -> k <> j -> Vf f k = k. by move => k kE ki kj; rewrite /f LfV// !variant_false. have pd:forall k, inc k n -> Vf f (Vf f k) = k. move => k kE; case (equal_or_not k i) => ki; first by rewrite ki pa pb. case (equal_or_not k j) => kj; first by rewrite kj pb pa. by rewrite !(pc _ kE ki kj). have sf: source f = n by rewrite /f;aw. have tf: target f = n by rewrite /f;aw. have ff: function f by apply: (lf_function ax). have bf: bijection f. split; split => //; first by rewrite sf => u v /pd {2} <- /pd {2} <- ->. rewrite sf tf => y ye;exists (Vf f y); [ Wtac | by rewrite pd]. by split => //; apply /permutationsP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)