Require Export Omega.
Require Export Even.
Require Export Max.
Require Export Min.
Require Export List.
Require Import Eqdep_dec.
Require Import Setoid.

Tactic Notation "apply" ":" constr(x) := pose proof x as HHH; first [
  refine HHH |
  refine (HHH _) |
  refine (HHH _ _) |
  refine (HHH _ _ _) |
  refine (HHH _ _ _ _) |
  refine (HHH _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _ _ _ _ _) |
  refine (HHH _ _ _ _ _ _ _ _ _ _ _ _ _ _)]; clear HHH.

Global Set Automatic Coercions Import.

Global Set Automatic Introduction.

Instance: @DefaultRelation N eq | 2.

Lemma lt_le_dec : ∀ n m : N, {n < m} + {m ≤ n}.
Proof.
 intros.
 case (le_lt_dec m n); auto.
Qed.

Lemma lt_z_two : 0 < 2.
Proof.
 auto.
Qed.

Lemma le_pred : ∀ n m : N, n ≤ m → pred n ≤ pred m.
Proof.
 simple induction n. simpl in |- ×. auto with arith.
  intros n0 Hn0. simple induction m. simpl in |- ×. intro H. inversion H.
 intros n1 H H0. simpl in |- ×. auto with arith.
Qed.

Lemma lt_mult_right : ∀ x y z : N, x < y → 0 < z → x × z < y × z.
Proof.
 intros x y z H H0.
 induction z as [| z Hrecz].
  elim (lt_irrefl _ H0).
 rewrite mult_comm.
 replace (y × S z) with (S z × y); auto with arith.
Qed.

Lemma le_mult_right : ∀ x y z : N, x ≤ y → x × z ≤ y × z.
Proof.
 intros x y z H.
 rewrite mult_comm. rewrite (mult_comm y).
 auto with arith.
Qed.

Lemma le_irrelevent : ∀ n m (H1 H2:le n m), H1=H2.
Proof.
 assert (∀ n (H1: le n n), H1 = le_n n).
  intros n H1.
  change H1 with (eq_rec n (fun a ⇒ a ≤ n) H1 _ (refl_equal n)).
  generalize (refl_equal n).
  revert H1.
  generalize n at 1 3 7.
  dependent inversion H1.
   apply K_dec_set.
    decide equality.
   reflexivity.
  intros; elimtype False; ω.
 induction m.
  dependent inversion H1.
  symmetry.
  apply H.
 dependent inversion H1.
  symmetry.
  apply H.
 intros H3.
 change H3 with (eq_rec (S m) (le n) (eq_rec n (fun n ⇒ n ≤ S m) H3 _ (refl_equal n)) _ (refl_equal (S m))).
 generalize (refl_equal n) (refl_equal (S m)).
 revert H3.
 generalize n at 1 2 7.
 generalize (S m) at 1 2 5 6.
 dependent inversion H3.
  intros; elimtype False; ω.
 intros e e0.
 assert (e':=e).
 assert (e0':=e0).
 revert e e0 l0.
 rewrite e', (eq_add_S _ _ e0').
 intros e.
 elim e using K_dec_set.
  decide equality.
 intros e0.
 elim e0 using K_dec_set.
  decide equality.
 simpl.
 intros l0.
 rewrite (IHm l l0).
 reflexivity.
Qed.

Lemma minus3:∀ (a b c:N),(c≤b≤a)-> a+(b-c)=b+(a-c).
Proof.
 intros a b d H.
 cut ((Z_of_nat a) + ((Z_of_nat b) - (Z_of_nat d)) = (Z_of_nat b) + ((Z_of_nat a) - (Z_of_nat d)))%Z.
  2:intuition.
 intro H1.
 elim H.
 intros H2 H3.
 set (H4:=(inj_minus1 b d H2)).
 rewrite<- H4 in H1.
 cut (d ≤a).
  intro H5.
  2:intuition.
 set (H6:=(inj_minus1 a d H5)).
 rewrite<- H6 in H1.
 intuition.
Qed.

Lemma minus4:∀ (a b c d:N), (d≤c≤b)->
  (a+b)+(c-d)=(a+c)+(b-d).
Proof.
 intros a b c0 d H.
 cut (((Z_of_nat a)+(Z_of_nat b))+((Z_of_nat c0)-(Z_of_nat d))=
   ((Z_of_nat a)+(Z_of_nat c0))+((Z_of_nat b)-(Z_of_nat d)))%Z.
  intro H0.
  2:intuition.
 elim H.
 intros H1 H2.
 set (H3:=(inj_minus1 c0 d H1)).
 rewrite<- H3 in H0.
 cut (d≤b).
  2:intuition.
 intro H4.
 set (H5:=(inj_minus1 b d H4)).
 rewrite<- H5 in H0.
 intuition.
Qed.

Fixpoint power (m : N) : N → N :=
  match m with
  | O ⇒ fun _ : N ⇒ 1
  | S n ⇒ fun x : N ⇒ power n x × x
  end.

Transparent sym_eq.
Transparent f_equal.

Notation Pair := (pair (B:=_)) (only parsing).
Notation Proj1 := (proj1 (B:=_)) (only parsing).
Notation Proj2 := (proj2 (B:=_)) (only parsing ).


Lemma not_r_sumbool_rec : ∀ (A B : Prop) (S : Set) (l r : S), ¬ B → ∀ H : {A} + {B},
 sumbool_rec (fun _ : {A} + {B} ⇒ S) (fun x : A ⇒ l) (fun x : B ⇒ r) H = l.
Proof.
 intros. elim H0.
 intros. reflexivity.
  intro. elim H. assumption.
Qed.

Lemma not_l_sumbool_rec : ∀ (A B : Prop) (S : Set) (l r : S), ¬ A → ∀ H : {A} + {B},
 sumbool_rec (fun _ : {A} + {B} ⇒ S) (fun x : A ⇒ l) (fun x : B ⇒ r) H = r.
Proof.
 intros. elim H0.
 intro. elim H. assumption.
  intros. reflexivity.
Qed.

Lemma POS_anti_convert : ∀ n : N, S n = Zpos (P_of_succ_nat n) :>Z.
Proof.
 simple induction n.
  simpl in |- ×.
  reflexivity.
 intros n0 H.
 simpl in |- ×.
 reflexivity.
Qed.

Lemma NEG_anti_convert : ∀ n : N, (- S n)%Z = Zneg (P_of_succ_nat n).
Proof.
 simple induction n.
  simpl in |- ×.
  reflexivity.
 intros n0 H.
 simpl in |- ×.
 reflexivity.
Qed.

Lemma lt_O_positive_to_nat : ∀ (p : positive) (m : N), 0 < m → 0 < Pmult_nat p m.
Proof.
 intro p.
 elim p.
   intros p0 H m H0.
   simpl in |- ×.
   auto with arith.
  intros p0 H m H0.
  simpl in |- ×.
  apply H.
  auto with arith.
 intros m H.
 simpl in |- ×.
 assumption.
Qed.

Lemma anti_convert_pred_convert : ∀ p : positive,
 p = P_of_succ_nat (pred (nat_of_P p)).
Proof.
 intro p.
 pattern p at 1 in |- ×.
 rewrite <- pred_o_P_of_succ_nat_o_nat_of_P_eq_id.
 cut (∃ n : N, nat_of_P p = S n).
  intro H.
  elim H; intros x H0.
  rewrite H0.
  elim x.
   simpl in |- ×.
   reflexivity.
  intros n H1.
  simpl in |- ×.
  rewrite Ppred_succ.
  reflexivity.
 ∃ (pred (nat_of_P p)).
 apply S_pred with 0.
 unfold nat_of_P in |- ×.
 apply lt_O_positive_to_nat.
 auto with arith.
Qed.

Lemma p_is_some_anti_convert : ∀ p : positive, ∃ n : N, p = P_of_succ_nat n.
Proof.
 intro p.
 ∃ (pred (nat_of_P p)).
 apply anti_convert_pred_convert.
Qed.

Lemma convert_is_POS : ∀ p : positive, nat_of_P p = Zpos p :>Z.
Proof.
 intro p.
 elim (p_is_some_anti_convert p).
 intros x H.
 rewrite H.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 apply POS_anti_convert.
Qed.

Lemma min_convert_is_NEG : ∀ p : positive, (- nat_of_P p)%Z = Zneg p.
Proof.
 intro p.
 elim (p_is_some_anti_convert p).
 intros x H.
 rewrite H.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 apply NEG_anti_convert.
Qed.

Lemma surj_eq:∀ (n m:N),
((Z_of_nat n)=(Z_of_nat m))%Z → n=m.
Proof.
 intros n m.
 intuition.
Qed.

Lemma surj_le:∀ (n m:N),
((Z_of_nat n)<=(Z_of_nat m))%Z → n≤m.
Proof.
 intros n m.
 intuition.
Qed.

Lemma surj_lt:∀ (n m:N),
((Z_of_nat n)<(Z_of_nat m))%Z → n<m.
Proof.
 intros n m.
 intuition.
Qed.

Lemma surj_not:∀ (n m:N),
((Z_of_nat n)<>(Z_of_nat m))%Z → n≠m.
Proof.
 intros n m.
 intuition.
Qed.

Lemma lt_lt_minus:∀(q p l:N),
q<l → p<q → p+(l-q)<l.
Proof.
 intros q p l H H0.
 intuition.
Qed.

Lemma inject_nat_convert :
 ∀ p : positive, Z_of_nat (nat_of_P p) = BinInt.Zpos p.
Proof.
 intros.
 elim (ZL4 p); intros.
 rewrite H.
 simpl in |- ×.
 apply (f_equal BinInt.Zpos).
 apply nat_of_P_inj.
 rewrite H.
 apply nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.

Definition Z_to_nat: ∀ (z:Z),(0≤z)%Z→N.
Proof.
 intros z.
 case z.
   intro H.
   exact 0.
  intros p H.
  exact (nat_of_P p).
 intros p H.
 cut False.
  intuition.
 intuition.
Defined.

Lemma Z_to_nat_correct:∀ (z:Z)(H:(0≤z)%Z),
   z=(Z_of_nat (Z_to_nat H)).
Proof.
 intro z.
 case z.
   intro H.
   unfold Z_to_nat.
   reflexivity.
  intros p H.
  unfold Z_to_nat.
  cut ( Z_of_nat (nat_of_P p)= Zpos p).
   intuition.
  apply inject_nat_convert.
 intros p H.
 cut False.
  intuition.
 intuition.
Qed.

Lemma Z_exh : ∀ z : Z, (∃ n : N, z = n) ∨ (∃ n : N, z = (- n)%Z).
Proof.
 intro z.
 elim z.
   left.
   ∃ 0.
   auto.
  intro p.
  left.
  ∃ (nat_of_P p).
  rewrite convert_is_POS.
  reflexivity.
 intro p.
 right.
 ∃ (nat_of_P p).
 rewrite min_convert_is_NEG.
 reflexivity.
Qed.

Lemma nats_Z_ind : ∀ P : Z → Prop,
 (∀ n : N, P n) → (∀ n : N, P (- n)%Z) → ∀ z : Z, P z.
Proof.
 intros P H H0 z.
 elim (Z_exh z); intro H1.
  elim H1; intros x H2.
  rewrite H2.
  apply H.
 elim H1; intros x H2.
 rewrite H2.
 apply H0.
Qed.

Lemma pred_succ_Z_ind : ∀ P : Z → Prop, P 0%Z →
 (∀ n : Z, P n → P (n + 1)%Z) → (∀ n : Z, P n → P (n - 1)%Z) → ∀ z : Z, P z.
Proof.
 intros P H H0 H1 z.
 apply nats_Z_ind.
  intro n.
  elim n.
   exact H.
  intros n0 H2.
  replace (S n0:Z) with (n0 + 1)%Z.
   apply H0.
   assumption.
  rewrite Znat.inj_S.
  reflexivity.
 intro n.
 elim n.
  exact H.
 intros n0 H2.
 replace (- S n0)%Z with (- n0 - 1)%Z.
  apply H1.
  assumption.
 rewrite Znat.inj_S.
 unfold Zsucc in |- ×.
 rewrite Zopp_plus_distr.
 reflexivity.
Qed.

Lemma Zmult_minus_distr_r : ∀ n m p : Z, (p × (n - m))%Z = (p × n - p × m)%Z.
Proof.
 intros n m p.
 rewrite Zmult_comm.
 rewrite Zmult_minus_distr_r.
 rewrite Zmult_comm.
 rewrite (Zmult_comm m p).
 reflexivity.
Qed.

Lemma Zodd_Zeven_min1 : ∀ x : Z, Zeven.Zodd x → Zeven.Zeven (x - 1).
Proof.
 intro x.
 elim x.
   simpl in |- ×.
   auto.
  simple induction p.
    simpl in |- ×.
    auto.
   intros p0 H H0.
   simpl in H0.
   tauto.
  simpl in |- *; auto.
 simple induction p.
   simpl in |- *; auto.
  simpl in |- *; auto.
 auto.
Qed.


Definition caseZ_diff (A : Type) (z : Z) (f : N → N → A) :=
  match z with
  | Z0 ⇒ f 0 0
  | Zpos m ⇒ f (nat_of_P m) 0
  | Zneg m ⇒ f 0 (nat_of_P m)
  end.


Lemma caseZ_diff_O : ∀ (A : Type) (f : N → N → A), caseZ_diff 0 f = f 0 0.
Proof.
 auto.
Qed.

Lemma caseZ_diff_Pos : ∀ (A : Type) (f : N → N → A) (n : N),
  caseZ_diff n f = f n 0.
Proof.
 intros A f n.
 elim n.
  reflexivity.
 intros n0 H.
 simpl in |- ×.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 reflexivity.
Qed.

Lemma caseZ_diff_Neg : ∀ (A : Type) (f : N → N → A) (n : N),
 caseZ_diff (- n) f = f 0 n.
Proof.
 intros A f n.
 elim n.
  reflexivity.
 intros n0 H.
 simpl in |- ×.
 rewrite nat_of_P_o_P_of_succ_nat_eq_succ.
 reflexivity.
Qed.

Lemma proper_caseZ_diff : ∀ (A : Type) (f : N → N → A),
 (∀ m n p q : N, m + q = n + p → f m n = f p q) →
 ∀ m n : N, caseZ_diff (m - n) f = f m n.
Proof.
 intros A F H m n.
 pattern m, n in |- ×.
 apply nat_double_ind.
   intro n0.
   replace (0%N - n0)%Z with (- n0)%Z.
    rewrite caseZ_diff_Neg.
    reflexivity.
   simpl in |- ×.
   reflexivity.
  intro n0.
  replace (S n0 - 0%N)%Z with (Z_of_nat (S n0)).
   rewrite caseZ_diff_Pos.
   reflexivity.
  simpl in |- ×.
  reflexivity.
 intros n0 m0 H0.
 rewrite (H (S n0) (S m0) n0 m0).
  rewrite <- H0.
  replace (S n0 - S m0)%Z with (n0 - m0)%Z.
   reflexivity.
  repeat rewrite Znat.inj_S.
  auto with zarith.
 auto with zarith.
Qed.

Lemma diff_Z_ind : ∀ P : Z → Prop, (∀ m n : N, P (m - n)%Z) → ∀ z : Z, P z.
Proof.
 intros P H z.
 apply nats_Z_ind.
  intro n.
  replace (Z_of_nat n) with (n - 0%N)%Z.
   apply H.
  simpl in |- ×.
  auto with zarith.
 intro n.
 replace (- n)%Z with (0%N - n)%Z.
  apply H.
 simpl in |- ×.
 reflexivity.
Qed.

Lemma Zlt_reg_mult_l : ∀ x y z : Z,
 (x > 0)%Z → (y < z)%Z → (x × y < x × z)%Z.
Proof.
 intros x y z H H0.
 case (Zcompare_Gt_spec x 0).
  unfold Zgt in H.
  assumption.
 intros x0 H1.
 cut (x = Zpos x0).
  intro H2.
  rewrite H2.
  unfold Zlt in H0.
  unfold Zlt in |- ×.
  cut ((Zpos x0 × y ?= Zpos x0 × z)%Z = (y ?= z)%Z).
   intro H3.
   exact (trans_eq H3 H0).
  apply Zcompare_mult_compat.
 cut (x = (x + - (0))%Z).
  intro H2.
  exact (trans_eq H2 H1).
 simpl in |- ×.
 apply (sym_eq (A:=Z)).
 exact (Zplus_0_r x).
Qed.

Lemma Zlt_opp : ∀ x y : Z, (x < y)%Z → (- x > - y)%Z.
Proof.
 intros x y H.
 red in |- ×.
 apply sym_eq.
 cut (Datatypes.Gt = (y ?= x)%Z).
  intro H0.
  cut ((y ?= x)%Z = (- x ?= - y)%Z).
   intro H1.
   exact (trans_eq H0 H1).
  exact (Zcompare_opp y x).
 apply sym_eq.
 exact (Zlt_gt x y H).
Qed.

Lemma Zlt_conv_mult_l : ∀ x y z : Z,
 (x < 0)%Z → (y < z)%Z → (x × y > x × z)%Z.
Proof.
 intros x y z H H0.
 cut (- x > 0)%Z.
  intro H1.
  cut (- x × y < - x × z)%Z.
   intro H2.
   cut (- (- x × y) > - (- x × z))%Z.
    intro H3.
    cut (- - (x × y) > - - (x × z))%Z.
     intro H4.
     cut ((- - (x × y))%Z = (x × y)%Z).
      intro H5.
      rewrite H5 in H4.
      cut ((- - (x × z))%Z = (x × z)%Z).
       intro H6.
       rewrite H6 in H4.
       assumption.
      exact (Zopp_involutive (x × z)).
     exact (Zopp_involutive (x × y)).
    cut ((- (- x × y))%Z = (- - (x × y))%Z).
     intro H4.
     rewrite H4 in H3.
     cut ((- (- x × z))%Z = (- - (x × z))%Z).
      intro H5.
      rewrite H5 in H3.
      assumption.
     cut ((- x × z)%Z = (- (x × z))%Z).
      intro H5.
      exact (f_equal Zopp H5).
     exact (Zopp_mult_distr_l_reverse x z).
    cut ((- x × y)%Z = (- (x × y))%Z).
     intro H4.
     exact (f_equal Zopp H4).
    exact (Zopp_mult_distr_l_reverse x y).
   exact (Zlt_opp (- x × y) (- x × z) H2).
  exact (Zlt_reg_mult_l (- x) y z H1 H0).
 exact (Zlt_opp x 0 H).
Qed.

Lemma Zgt_not_eq : ∀ x y : Z, (x > y)%Z → x ≠ y.
Proof.
 intros x y H.
 cut (y < x)%Z.
  intro H0.
  cut (y ≠ x).
   intro H1.
   red in |- ×.
   intro H2.
   cut (y = x).
    intro H3.
    apply H1.
    assumption.
   exact (sym_eq H2).
  exact (Zorder.Zlt_not_eq y x H0).
 exact (Zgt_lt x y H).
Qed.

Lemma Zmult_absorb : ∀ x y z : Z,
 x ≠ 0%Z → (x × y)%Z = (x × z)%Z → y = z.
Proof.
 intros x y z H H0.
 case (dec_eq y z).
  intro H1.
  assumption.
 intro H1.
 case (not_Zeq y z).
   assumption.
  intro H2.
  case (not_Zeq x 0).
    assumption.
   intro H3.
   elimtype False.
   cut (x × y > x × z)%Z.
    intro H4.
    cut ((x × y)%Z ≠ (x × z)%Z).
     intro H5.
     apply H5.
     assumption.
    exact (Zgt_not_eq (x × y) (x × z) H4).
   exact (Zlt_conv_mult_l x y z H3 H2).
  intro H3.
  elimtype False.
  cut (x × y < x × z)%Z.
   intro H4.
   cut ((x × y)%Z ≠ (x × z)%Z).
    intro H5.
    apply H5.
    assumption.
   exact (Zorder.Zlt_not_eq (x × y) (x × z) H4).
  apply Zlt_reg_mult_l.
   exact (Zlt_gt 0 x H3).
  assumption.
 intro H2.
 apply False_ind.
 cut (x × z < x × y)%Z.
  intro H3.
  cut ((x × z)%Z ≠ (x × y)%Z).
   intro H4.
   apply H4.
   apply (sym_eq (A:=Z)).
   assumption.
  exact (Zorder.Zlt_not_eq (x × z) (x × y) H3).
 apply False_ind.
 case (not_Zeq x 0).
   assumption.
  intro H3.
  cut (x × z > x × y)%Z.
   intro H4.
   cut ((x × z)%Z ≠ (x × y)%Z).
    intro H5.
    apply H5.
    apply (sym_eq (A:=Z)).
    assumption.
   exact (Zgt_not_eq (x × z) (x × y) H4).
  exact (Zlt_conv_mult_l x z y H3 H2).
 intro H3.
 cut (x × z < x × y)%Z.
  intro H4.
  cut ((x × z)%Z ≠ (x × y)%Z).
   intro H5.
   apply H5.
   apply (sym_eq (A:=Z)).
   assumption.
  exact (Zorder.Zlt_not_eq (x × z) (x × y) H4).
 apply Zlt_reg_mult_l.
  exact (Zlt_gt 0 x H3).
 auto.
Qed.

Section Well_foundedT.

 Variable A : Type.
 Variable R : A → A → Prop.

 Inductive Acc : A → Prop :=
     Acc_intro : ∀ x : A, (∀ y : A, R y x → Acc y) → Acc x.
End Well_foundedT.

Section AccT.
Variable A : Type.
Definition well_founded (P : A → A → Prop) := ∀ a : A, Acc _ P a.
End AccT.
Implicit Arguments Acc [A].

Section IndT.
Variable A : Type.
Variable R : A → A → Prop.
Section AccIter.
  Variable P : A → Type.
  Variable F : ∀ x : A, (∀ y : A, R y x → P y) → P x.
Lemma Acc_inv : ∀ x : A, Acc R x → ∀ y : A, R y x → Acc R y.
Proof.
 destruct 1; trivial.
 Defined.

  Fixpoint Acc_iter (x : A) (a : Acc R x) {struct a} :
   P x := F x (fun (y : A) (h : R y x) ⇒ Acc_iter y (Acc_inv x a y h)).

 End AccIter.

Hypothesis Rwf : well_founded A R.

Theorem well_founded_induction_type :
 ∀ P : A → Type,
 (∀ x : A, (∀ y : A, R y x → P y) → P x) → ∀ a : A, P a.
Proof.
 Proof.
 intros; apply (Acc_iter P); auto.
 Defined.
End IndT.

Section InductionT.
Variable A : Type.

Variable f : A → N.
Definition ltof (a b : A) := f a < f b.

Theorem well_founded_ltof : well_founded A ltof.
Proof.
 red in |- ×.
 cut (∀ (n : N) (a : A), f a < n → Acc ltof a).
  intros H a; apply (H (S (f a))); auto with arith.
 induction n.
  intros; absurd (f a < 0); auto with arith.
 intros a ltSma.
 apply Acc_intro.
 unfold ltof in |- *; intros b ltfafb.
 apply IHn.
 apply lt_le_trans with (f a); auto with arith.
Qed.

Theorem induction_ltof2T : ∀ P : A → Type,
 (∀ x : A, (∀ y : A, ltof y x → P y) → P x) → ∀ a : A, P a.
Proof.
 exact (well_founded_induction_type A ltof well_founded_ltof).
Defined.
End InductionT.

Section InductionTT.
Lemma lt_wf_rect : ∀ (p : N) (P : N → Type),
 (∀ n : N, (∀ m : N, m < n → P m) → P n) → P p.
Proof.
 exact (fun (p : N) (P : N → Type) (F : ∀ n : N, (∀ m : N, m < n → P m) → P n) ⇒
   induction_ltof2T N (fun m : N ⇒ m) P F p).
Defined.
End InductionTT.

Fixpoint positive_rect2_helper
 (P : positive → Type)
 (c1 : ∀ p : positive, P (Psucc p) → P p → P (xI p))
 (c2 : ∀ p : positive, P p → P (xO p))
 (c3 : P 1%positive)
 (b : bool) (p : positive) {struct p} : P (if b then Psucc p else p) :=
 match p with
 | xH ⇒ match b with true ⇒ c2 _ c3 | false ⇒ c3 end
 | xO p' ⇒ match b with
             | true ⇒ c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _)
             | false ⇒ c2 _ (positive_rect2_helper P c1 c2 c3 false _)
             end
 | xI p' ⇒ match b with
             | true ⇒ c2 _ (positive_rect2_helper P c1 c2 c3 true _)
             | false ⇒c1 _ (positive_rect2_helper P c1 c2 c3 true _) (positive_rect2_helper P c1 c2 c3 false _)
             end
 end.

Definition positive_rect2
 (P : positive → Type)
 (c1 : ∀ p : positive, P (Psucc p) → P p → P (xI p))
 (c2 : ∀ p : positive, P p → P (xO p))
 (c3 : P 1%positive) (p : positive) : P p :=
positive_rect2_helper P c1 c2 c3 false p.

Lemma positive_rect2_helper_bool : ∀ P c1 c2 c3 p,
positive_rect2_helper P c1 c2 c3 true p =
positive_rect2_helper P c1 c2 c3 false (Psucc p).
Proof.
 intros P c1 c2 c3.
 induction p; try reflexivity.
 simpl.
 rewrite IHp.
 reflexivity.
Qed.

Lemma positive_rect2_red1 : ∀ P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xI p) =
c1 p (positive_rect2 P c1 c2 c3 (Psucc p)) (positive_rect2 P c1 c2 c3 p).
Proof.
 intros P c1 c2 c3 p.
 unfold positive_rect2.
 simpl.
 rewrite positive_rect2_helper_bool.
 reflexivity.
Qed.

Lemma positive_rect2_red2 : ∀ P c1 c2 c3 p,
positive_rect2 P c1 c2 c3 (xO p) =
c2 p (positive_rect2 P c1 c2 c3 p).
Proof.
 reflexivity.
Qed.

Lemma positive_rect2_red3 : ∀ P c1 c2 c3,
positive_rect2 P c1 c2 c3 (xH) = c3.
Proof.
 reflexivity.
Qed.

Fixpoint iterateN A (f:A → A) (z:A) (n:N) : list A :=
match n with
 O ⇒ nil
|S m ⇒ z :: (iterateN A f (f z) m)
end.
Lemma iterateN_f : ∀ A f (z:A) n, iterateN f (f z) n = map f (iterateN f z n).
Proof.
 intros A f z n.
 revert f z.
 induction n.
  reflexivity.
 simpl.
 intros f z.
 rewrite <- IHn.
 reflexivity.
Qed.


Lemma iff_under_forall {X} (P Q: X → Prop): (∀ x, P x ↔ Q x) → ((∀ x, P x) ↔ (∀ x, Q x)).
Proof. firstorder. Qed.

Lemma conjunction_under_forall {X} (P Q: X → Prop): ((∀ x, P x) ∧ (∀ x, Q x)) ↔ (∀ x, P x ∧ Q x).
Proof. firstorder. Qed.