proposition: Lemma odd_lift_perm : forall n i j s, @lift_perm n i j s = odd i (+) odd j (+) s :> bool.
proof: Proof. move=> n i j s; 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 bigops.big_nil lift_perm1 !odd_perm1. rewrite bigops.big_cons odd_mul_tperm -(lift_permM _ j) odd_permM {}IHts //. congr (_ (+) _); rewrite (_ : _ j _ = tperm (lift j t.1) (lift j t.2)). by rewrite odd_tperm (inj_eq (@lift_inj _ _)). apply/permP=> k; case: (unliftP j k) => [k'|] ->. rewrite lift_perm_lift inj_tperm //; exact: lift_inj. by rewrite lift_perm_id tpermD // eq_sym neq_lift. suff{i j s} odd_lift0: forall 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. move=> k; elim: {k}(k : nat) {1 3}k (erefl (k : nat)) => [|m IHm] k def_k. rewrite (_ : k = ord0) ?lift_perm1 ?odd_perm1 //; exact: 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 (_ : _ k _ = tperm j k). 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 eq_sym; case: eqP. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms