proposition: Lemma tc5ai s l p : validtc5 l -> valid63 p -> tc5i l s p = false -> tc5i l (tc5a l s p) p = true.
proof: Proof. intros H Hp. assert (Hp1: (Zpos p <= 63)%Z); auto. case (validtc5_inv _ H); clear H. intros p1 [l1 [H1 [[H2 | [H2 | [H2 | [H2 | H2]]]] H3]]]; rewrite H1; rewrite H2; clear H1 H2; case s; unfold tc5i, tc5a; auto; intros; apply tc6ai; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik