proposition: Lemma chain_cases : forall p : nat, 0 < p -> {q : nat | q < p /\ two <= q} + {l : nat | p = two_power l} + {p = three}.
proof: Proof. refine (fun p _H => match eq_nat_dec p three with | left h => inright _ h | right n => match log2_r p _ with | existS l b => match b with | left _ => inleft _ (inr _ (exist _ l _)) | right a => match gamma with | mkstrat s => match s p _ with | exist q _ => inleft _ (inl _ (exist _ q _)) end end end end end); auto. case (le_or_lt (S four) p); [ auto with arith | intro H2 ]. case (enum4 p H2); intro. absurd (0 < p); [ rewrite H; auto with arith | auto with arith ]. elim H; intro H3. absurd (p = one); [ replace one with (two_power 0) | auto with arith ]. apply holes_in_powers with l; elim a; auto with arith. simpl in |- *; auto with arith. elim H3; intro H4. absurd (p = two); [ replace two with (two_power one) | auto with arith ]. apply holes_in_powers with l; elim a; auto with arith. simpl in |- *; auto with arith. elim H4; intro H5. elim (n H5). absurd (p = four); [ replace four with (two_power two) | auto with arith ]. apply holes_in_powers with l; elim a; auto with arith. simpl in |- *; auto with arith. Qed.
imports: monoid spec Constants machine Euclid Le_lt_compl euclid shift two_power log2_spec develop Arith Peano_dec Compare_dec strategies Mult_compl Wf_nat Wf_compl