proposition: Lemma half_aux_succ : forall x, half_aux (S x) = (S (snd (half_aux x)), fst (half_aux x)).
proof: Proof. intros. remember (half_aux x) as h. destruct h as (f,s); simpl in *. unfold half_aux in *. rewrite recursion_succ, <- Heqh; simpl; f_equiv'. Qed.
imports: Bool RelationPairs NStrongRec