fact: Fixpoint naive_int63it_aux (m : nat) (p : positive) (c : int) (l1 : list cube) (l2 : list orientation) (a : A) {struct m} := let a1 := if int63i c p then next a l1 l2 p else a in match m with | O => a1 | S m1 => naive_int63it_aux m1 (Pos.succ p) c l1 l2 a1 end.
imports: PrimInt63 Cyclic63 List BasicRubik