proposition: Theorem make_listtc5ir l p c l1 l2 ll : validtc5 (rev l) -> valid63 p -> tc5i (rev l) c p = true -> In (l ++ l1, l2, p) (tc5it _ make_list l1 l2 ll c).
proof: Proof. case c. now unfold tc5i; intros _ _ HH; discriminate. intros cc1 cc2 cc3 cc4 cc5 HH Hp. case (validtc5_inv _ HH); clear HH. intros p1 (l3, (HH, (HH1, Hl3))). rewrite <- (rev_involutive l). rewrite HH; simpl rev; clear HH. rewrite rev_unit; rewrite rev_involutive; case HH1; [intros HH2 | intros [HH2 | [HH2 | [HH2 | HH2]]]]; rewrite HH2; clear HH1 HH2; simpl; intros HH; rewrite app_ass; simpl app. - apply make_listtc6ir; auto; rewrite rev_involutive; auto. - apply make_listtc6irI; apply make_listtc6ir; auto; rewrite rev_involutive; auto. - do 2 (apply make_listtc6irI); apply make_listtc6ir; auto; rewrite rev_involutive; auto. - do 3 (apply make_listtc6irI); apply make_listtc6ir; auto; rewrite rev_involutive; auto. - do 4 (apply make_listtc6irI); apply make_listtc6ir; auto; rewrite rev_involutive; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik