proposition: Lemma tc2_get_number_equiv s s1 s2 l1 l2 : valid_state s -> valid_pair (s1, s2) -> pstates_equiv (s1,s2) (l1,l2) -> get_number s s1 s2 = tc2_get_number s l1 l2.
proof: Proof. intros Hg (Hg1, Hg2) (H1, H2); simpl in Hg1, Hg2, H1, H2. unfold get_number, tc2_get_number. rewrite (in_states_equiv s1 l1); auto. rewrite (in_states_equiv s2 l2); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max