proposition: Lemma treeify_aux_spec n (p:bool) : treeify_invariant (ifpred p (Pos.to_nat n)) (treeify_aux p n).
proof: Proof. revert p. induction n as [n|n|]; intros p; simpl treeify_aux. - eapply treeify_cont_spec; [ apply (IHn false) | apply (IHn p) | ]. rewrite Pos2Nat.inj_xI. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. destruct p; simpl; intros; rewrite Nat.add_0_r; trivial. now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial. - eapply treeify_cont_spec; [ apply (IHn p) | apply (IHn true) | ]. rewrite Pos2Nat.inj_xO. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. rewrite <- Nat.add_succ_r, Nat.succ_pred by trivial. destruct p; simpl; intros; rewrite Nat.add_0_r; trivial. symmetry. now apply Nat.add_pred_l. - destruct p; [ apply treeify_zero_spec | apply treeify_one_spec ]. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat