proposition: Theorem make_listtc2fold a c : tc2it _ next a c = fold_left nextp (tc2it _ make_list nil c) a.
proof: Proof. case c. now reflexivity. intros cc1 cc2; unfold tc2it. repeat rewrite make_listto5fold. repeat rewrite <- fold_left_app. repeat rewrite <- app_ass. repeat rewrite <- make_listto5irA. repeat rewrite <- app_nil_end. reflexivity. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik