proposition: Lemma tc2ai s l l1 p : validtc2 l -> validto5 l1 -> valid63 p -> tc2i l l1 p s = false -> tc2i l l1 p (tc2a l l1 p s) = true.
proof: Proof. intros Hl Hl1 Hp. assert (Hp1: (Zpos p <= 63)%Z); auto. case (validtc2_inv _ Hl); clear Hl. intros p1 [l2 [H1 [[H2 | H2] H3]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc2i, tc2a; auto; intros; apply to5ai; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik