proposition: Lemma check63_all c : int63all c = true -> forall s, (Zpos s <= 63)%Z -> int63i c s = true.
proof: Proof. unfold int63all. generalize (phi_compare63 c 9223372036854775807); case compare; try (intros; discriminate). intros H1 _ s Hs. assert (F0: (Zpos s <= 63)%Z); auto with zarith. generalize (spec_int63i c s F0); rewrite H1. case int63i; auto. change (to_Z 9223372036854775807)%Z with (9223372036854775807)%Z. generalize s Hs; clear s Hs F0. do 6 (intros s; case s; clear s; [idtac|idtac| match goal with |- context[?X = 0%Z] => change X with 1%Z end; intros; discriminate]); try (now intros p HH; contradict HH; auto with zarith). Qed.
imports: PrimInt63 Cyclic63 List BasicRubik