proposition: Theorem half_aux_spec : forall n, n == fst (half_aux n) + snd (half_aux n).
proof: Proof. apply induction. - intros x x' Hx. setoid_rewrite Hx; auto with *. - rewrite half_aux_0; simpl; rewrite add_0_l; auto with *. - intros. rewrite half_aux_succ. simpl. rewrite add_succ_l, add_comm; auto. now f_equiv. Qed.
imports: Bool RelationPairs NStrongRec