proposition: Lemma treeify_aux_rb n : exists d, forall (b:bool), treeify_rb_invariant (ifpred b (Pos.to_nat n)) d (treeify_aux b n).
proof: Proof. induction n as [n (d,IHn)|n (d,IHn)| ]. - exists (S d). intros b. eapply treeify_cont_rb; [ apply (IHn false) | apply (IHn b) | ]. rewrite Pos2Nat.inj_xI. assert (H := Pos2Nat.is_pos n). apply Nat.neq_0_lt_0 in H. destruct b; simpl; intros; rewrite Nat.add_0_r; trivial. now rewrite <- Nat.add_succ_r, Nat.succ_pred; trivial. - exists (S d). intros b. eapply treeify_cont_rb; [ apply (IHn b) | 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 b; simpl; intros; rewrite Nat.add_0_r; trivial. symmetry. now apply Nat.add_pred_l. - exists 0; destruct b; [ apply treeify_zero_rb | apply treeify_one_rb ]. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat