proposition: Lemma naive_auxS m p c l1 l2 a : naive_int63it_aux (S m) p c l1 l2 a = naive_int63it_aux m (Pos.succ p) c l1 l2 (if int63i c p then next a l1 l2 p else a).
proof: Proof. unfold naive_int63it_aux; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik