proposition: Lemma circPermPerm {T:Type} {m:nat} : forall (n : nat) (cp : cartesianPower T (S (S m))), circPermNCP (S (S (S n))) cp = circPermNCP 1 (circPermNCP (S (S n)) cp).
proof: Proof. intros n cp. rewrite circPermNCPOK. apply eq_sym. rewrite circPermNCPOK. rewrite <- circPermNCP0. apply circPermNConsTlOK. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality