proposition: Theorem make_listto1ir l1 l2 p c l3 l4 ll : validtc4 (rev l1) -> validto1 (rev l2) -> valid63 p -> to1i (rev l2) c (rev l1) p = true -> In (l1++l3,l2++l4,p) (to1it _ make_list l3 l4 ll c).
proof: Proof. case c. now unfold to1i; intros _ _ _ HH; discriminate. intros cc1 cc2 cc3 Hl1 Hl2 Hp. generalize Hl2; case l2; try (intros; discriminate). simpl rev; intros o1 l5; case l5; clear l5. 2: intros o2 l5; unfold validto1; simpl rev; repeat rewrite app_length; simpl length; repeat rewrite <-plus_n_Sm; intros; discriminate. simpl app; intros _; case o1; simpl; intros HH. - apply make_listtc4ir; auto. - apply make_listtc4irI; apply make_listtc4ir; auto. - do 2 (apply make_listtc4irI); apply make_listtc4ir; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik