proposition: Lemma InCPOCP {n : nat} : forall p (cp : cartesianPower positive (S (S n))), InCP p cp <-> InCP p (OCP cp).
proof: Proof. intros p cp. unfold OCP. unfold OCPAux. unfold InCP. elim_eq_rect; simpl. induction n. rewrite CPLOK. assert (HPerm1 := Permuted_sort (CPToList cp)); simpl in HPerm1. assert (HPerm2 := HPerm1); apply Permutation.Permutation_sym in HPerm2. assert (HInOK : In p (sort (fst cp :: snd cp :: nil)) <-> In p (fst cp :: snd cp :: nil)) by (split; intro HIn; try (apply Permutation.Permutation_in with (sort (fst cp :: snd cp :: nil)); assumption); apply Permutation.Permutation_in with (fst cp :: snd cp :: nil); assumption). split; intro HIn. apply HInOK; simpl; assumption. apply HInOK in HIn; simpl in HIn; assumption. clear IHn. rewrite CPLOK. set (sscp := (nat_rect (fun n : nat => cartesianPower positive (S n) -> list positive) (fun cp0 : cartesianPower positive 1 => cp0 :: nil) (fun (n : nat) (IHn : cartesianPower positive (S n) -> list positive) (cp0 : cartesianPower positive (S (S n))) => fst cp0 :: IHn (tailCP cp0)) n (tailCP (snd cp)))). assert (HPerm := Permuted_sort (fst cp :: fst (snd cp) :: sscp)). split; intro HIn. elim HIn; clear HIn; intro HIn. subst. apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption. apply in_eq. elim HIn; clear HIn; intro HIn. subst. apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption. apply in_cons. apply in_eq. apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption. do 2 (apply in_cons). assumption. apply Permutation.Permutation_sym in HPerm. assert (HInOKAux := Permutation.Permutation_in). assert (HInOK := HInOKAux positive (sort (fst cp :: fst (snd cp) :: sscp)) (fst cp :: fst (snd cp) :: sscp) p HPerm HIn); clear HInOKAux; clear HIn. rename HInOK into HIn. assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms