proposition: Lemma Unshift : forall n : nat, {m : nat & {n = shift m} + {n = S (shift m)}}.
proof: Proof. refine (fun n => match eucl_dev two _ n with | divex q r g e => existS _ q _ end). unfold two in |- *; auto. elim (zerop r); intro e0; [ left | right ]. rewrite e; rewrite e0; rewrite <- plus_n_O; unfold shift in |- *; auto with arith. cut (r = 1). intro eq1. rewrite e; rewrite eq1. unfold shift in |- *. rewrite <- plus_n_1; auto with arith. case (enum1 r). auto with arith. intro e'; absurd (0 < r); [ elim e'; auto with arith | auto with arith ]. auto with arith. Qed.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid Compare_dec