proposition: Lemma tc6ai: forall s l p, validtc6 l -> valid63 p -> tc6i l s p = false -> tc6i l (tc6a l s p) p = true.
proof: Proof. intros s l p H Hp. assert (Hp1: (Zpos p <= 63)%Z); auto. case (validtc6_inv _ H); clear H. intros p1 [H1 [H2 | [H2 | [H2 | [H2 | [H2 | H2]]]]]]; rewrite H1 , H2; case s; simpl; intros; apply int63ai; auto with zarith; apply int63_0; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik