proposition: Lemma OCPTlOK {n : nat} : forall (cp : cartesianPower positive (S (S (S n)))), headCP cp = headCP (OCP cp) -> OCP (tailCP cp) = tailCP (OCP cp).
proof: Proof. intros cp Hhd. apply CPLOCPTlOK in Hhd. apply CPLCP; assumption. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms