proposition: Lemma CPToSSHdTl {m:nat} : forall (cp : cartesianPower positive (S (S m))), CPToSS cp = S.add (headCP cp) (CPToSS (tailCP cp)).
proof: Proof. simpl; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets