proposition: Lemma odd_lift_perm i j s : lift_perm i j s = odd i (+) odd j (+) s :> bool.
proof: Proof. rewrite -{1}(mul1g s) -(lift_permM _ j) odd_permM. congr (_ (+) _); last first. case: (prod_tpermP s) => ts ->{s} _. elim: ts => [|t ts IHts] /=; first by rewrite big_nil lift_perm1 !odd_perm1. rewrite big_cons odd_mul_tperm -(lift_permM _ j) odd_permM {}IHts //. congr (_ (+) _); transitivity (tperm (lift j t.1) (lift j t.2)); last first. by rewrite odd_tperm (inj_eq (pcan_inj (liftK j))). congr odd_perm; apply/permP=> k; case: (unliftP j k) => [k'|] ->. by rewrite lift_perm_lift inj_tperm //; apply: lift_inj. by rewrite lift_perm_id tpermD // eq_sym neq_lift. suff{i j s} odd_lift0 (k : 'I_n.+1): lift_perm ord0 k 1 = odd k :> bool. rewrite -!odd_lift0 -{2}invg1 -lift_permV odd_permV -odd_permM. by rewrite lift_permM mulg1. elim: {k}(k : nat) {1 3}k (erefl (k : nat)) => [|m IHm] k def_k. by rewrite (_ : k = ord0) ?lift_perm1 ?odd_perm1 //; apply: val_inj. have le_mn: m < n.+1 by [rewrite -def_k ltnW]; pose j := Ordinal le_mn. rewrite -(mulg1 1)%g -(lift_permM _ j) odd_permM {}IHm // addbC. rewrite (_ : _ 1 = tperm j k); first by rewrite odd_tperm neq_ltn/= def_k leqnn. apply/permP=> i; case: (unliftP j i) => [i'|] ->; last first. by rewrite lift_perm_id tpermL. apply: ord_inj; rewrite lift_perm_lift !permE /= eq_sym -if_neg neq_lift. rewrite fun_if -val_eqE /= def_k /bump ltn_neqAle andbC. case: leqP => [_ | lt_i'm] /=; last by rewrite -if_neg neq_ltn leqW. by rewrite add1n eqSS; case: eqVneq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)