proposition: Lemma nthCircPermNAny {T:Type} {m:nat} : forall (cp : cartesianPower T (S (S m))) (Default : T) id n, id + n <= S m -> nthCP (S id + n) cp Default = nthCP (S id) (circPermNCP n cp) Default.
proof: Proof. intros cp Default id n Hle; revert cp; induction n; intro cp. rewrite plus_n_0; simpl; reflexivity. rewrite circPermNCPOK. assert (H : id + n <= S m) by (apply le_Sn_le; rewrite plus_n_Sm; assumption). assert (H' : id + n <= m) by (apply le_S_n; transitivity (id + S n); intuition). rewrite <- IHn; try assumption. rewrite <- plus_n_Sm. apply nthCircPerm2Eq; assumption. Qed.
imports: Arith NArith List Sorting Coq.Program.Equality