proposition: Lemma positive_4step_ind : forall P : positive -> Prop, P 1%positive -> P 2%positive -> P 3%positive -> (forall p, P p -> P (xO (xO p)) /\ P (xI (xO p)) /\ P (xO (xI p)) /\ P (xI (xI p))) -> forall p, P p.
proof: Proof. intros P H H0 H1 H2 p; assert (P p /\ P (xO p) /\ P (xI p)). - induction p. + repeat split; try tauto. * destruct (H2 p);tauto. * destruct (H2 p);tauto. + repeat split; try tauto. * destruct (H2 p);tauto. * destruct (H2 p);tauto. + repeat split;tauto. - tauto. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)