fact: Definition pos_peano_ind_beta_pos_succ (P : Pos -> Type) (a : P 1) (f : forall p, P p -> P (pos_succ p)) (p : Pos) : pos_peano_ind P a f (pos_succ p) = f _ (pos_peano_ind P a f p).
imports: Basics.Overture Basics.Tactics Basics.Decidable Spaces.Nat.Core