fact: Fixpoint positive_rect2_helper (P : positive -> Type) (c1 : forall p : positive, P (Pos.succ p) -> P p -> P (xI p)) (c2 : forall p : positive, P p -> P (xO p)) (c3 : P 1%positive) (b : bool) (p : positive) {struct p} : P (if b then Pos.succ 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.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid