proposition: Lemma permut_cons_rev : forall h p q, permut (h :: p) (h :: q) -> permut p q.
proof: Proof. intros h p q [Hl f Hf Hpq]. assert (H2: length (h :: p) = 1 + length p). easy. simple refine (Permut _ _ _ _ _ _). - now injection Hl. - intros k. destruct (split (cast_ord H2 (f (rshift 1 k)))) as [_|k']. destruct (split (cast_ord H2 (f (@ord0 (length p))))) as [_|k']. apply k. apply k'. apply k'. - set (g := fun (k : ordinal (length p)) => match split (cast_ord H2 (invF Hf (rshift 1 k))) with | inl _ => match split (cast_ord H2 (invF Hf (@ord0 (length p)))) with | inl _ => k | inr k' => k' end | inr k' => k' end). apply (@can_inj _ _ _ g). intros k. unfold g. clear g. destruct (splitP (cast_ord H2 (f (rshift 1 k)))) as [k1 Hk1|k1 Hk1]. + replace (nat_of_ord k1) with O in Hk1 by now destruct k1 as [[|k1] H]. destruct (splitP (cast_ord H2 (f (@ord0 (length p))))) as [k2 Hk2|k2 Hk2]. replace (nat_of_ord k2) with O in Hk2 by now destruct k2 as [[|k2] H]. exfalso. rewrite <- Hk2 in Hk1. apply ord_inj in Hk1. apply cast_ord_inj in Hk1. now apply Hf in Hk1. replace (invF Hf (rshift 1 k2)) with (@ord0 (length p)). destruct (splitP (cast_ord H2 (@ord0 (length p)))) as [k3 Hk3|k3 Hk3]. 2: easy. replace (invF Hf (@ord0 (length p))) with (rshift 1 k). destruct (splitP (cast_ord H2 (rshift 1 k))) as [k4 Hk4|k4 Hk4]. now destruct k4 as [[|k4] H]. apply ord_inj. now injection Hk4. apply Hf. rewrite f_invF. now apply ord_inj. apply Hf. rewrite f_invF. now apply ord_inj. + replace (invF Hf (rshift 1 k1)) with (rshift 1 k). destruct (splitP (cast_ord H2 (rshift 1 k))) as [k2 Hk2|k2 Hk2]. now destruct k2 as [[|k2] H]. apply ord_inj. now injection Hk2. apply Hf. rewrite f_invF. now apply ord_inj. - intros k. destruct (splitP (cast_ord H2 (f (rshift 1 k)))) as [k1 Hk1|k1 Hk1]. + replace (nat_of_ord k1) with O in Hk1 by now destruct k1 as [[|k1] H]. destruct (splitP (cast_ord H2 (f (@ord0 (length p))))) as [k2 Hk2|k2 Hk2]. replace (nat_of_ord k2) with O in Hk2 by now destruct k2 as [[|k2] H]. exfalso. rewrite <- Hk2 in Hk1. apply ord_inj in Hk1. apply cast_ord_inj in Hk1. now apply Hf in Hk1. destruct (splitP (cast_ord H2 (f (rshift 1 k)))) as [k3 Hk3|k3 Hk3]. 2: now rewrite Hk1 in Hk3. change (onth (rshift 1 k) (h :: p) = onth (ssrnat.addn 1 k2) (h :: q)). rewrite Hpq. simpl in Hk1, Hk2. simpl (length (h :: p)). rewrite Hk1, <- Hk2. now rewrite <- Hpq. + destruct (splitP (cast_ord H2 (f (rshift 1 k)))) as [k2 Hk2|k2 Hk2]. rewrite Hk1 in Hk2. now destruct k2 as [[|k2] H]. simpl. change (onth (rshift 1 k) (h :: p) = onth (ssrnat.addn 1 k2) (h :: q)). rewrite <- Hk2. apply Hpq. Qed.
imports: Coq(List Arith ZArith Psatz) mathcomp.ssreflect(ssrfun ssrbool fintype)