proposition: Theorem make_listto5ir l1 l2 p c l3 l4 ll : validtc4 (rev l1) -> validto5 (rev l2) -> valid63 p -> to5i (rev l2) c (rev l1) p = true -> In (l1++l3,l2++l4,p) (to5it _ make_list l3 l4 ll c).
proof: Proof. case c. now unfold to5i; intros _ _ _ HH; discriminate. intros cc1 cc2 cc3 Hl1 Hl2 Hp. pattern l2 at 2; rewrite <- (rev_involutive l2). generalize Hl2; case (rev l2); try (intros; discriminate). simpl rev; intros o1 l5; case o1; clear o1; intros Hl5; simpl; intros HH; rewrite app_ass. - apply make_listto4ir; auto; rewrite rev_involutive; injection Hl5; auto. - apply make_listto4irI; apply make_listto4ir; auto; rewrite rev_involutive; injection Hl5; auto. - do 2 (apply make_listto4irI); apply make_listto4ir; auto; rewrite rev_involutive; injection Hl5; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik