proposition: Lemma circPermNConsOK {T:Type} {n:nat} : forall (cp : cartesianPower T (S n)) (t1 t2 : T), circPermNCP (S n) (consTailCP (consTailCP cp t1) t2) = consHeadCP t1 (consHeadCP t2 cp).
proof: Proof. induction n; intros cp t1 t2. simpl; reflexivity. clear IHn. assert (H := circPermNId (consHeadCP t1 (consHeadCP t2 cp))); rewrite H; clear H. apply eq_sym. rewrite circPermNCPOK. assert (H : headCP (consHeadCP t1 (consHeadCP t2 cp)) = t1) by (simpl; reflexivity); rewrite H; clear H. assert (H : tailCP (consHeadCP t1 (consHeadCP t2 cp)) = consHeadCP t2 cp) by (simpl; reflexivity); rewrite H; clear H. rewrite circPermNCPOK. assert (H : headCP (consTailCP (consHeadCP t2 cp) t1) = t2) by (simpl; reflexivity); rewrite H; clear H. assert (H : tailCP (consTailCP (consHeadCP t2 cp) t1) = consTailCP cp t1) by (simpl; reflexivity); rewrite H; clear H. reflexivity. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality