proposition: Lemma peano_equiv (P:positive->Type) (a:P 1) (f:forall p, P p -> P (succ p)) p : PeanoView_iter P a f p (peanoView p) = peano_rect P a f p.
proof: Proof. revert P a f. induction p as [|p IHp] using peano_rect. - trivial. - intros; simpl. rewrite peano_rect_succ. rewrite (PeanoViewUnique _ (peanoView (succ p)) (PeanoSucc _ (peanoView p))). simpl; now f_equal. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef