proposition: Theorem half_aux_spec2 : forall n, fst (half_aux n) == snd (half_aux n) \/ fst (half_aux n) == S (snd (half_aux n)).
proof: Proof. apply induction. - intros x x' Hx. setoid_rewrite Hx; auto with *. - rewrite half_aux_0; simpl. auto with *. - intros. rewrite half_aux_succ; simpl. destruct H; auto with *. right; now f_equiv. Qed.
imports: Bool RelationPairs NStrongRec