proposition: Lemma dicho_aux_lt : forall p, 3 < p -> xO (dicho_aux p) <= p.
proof: Proof. intro p; pattern p; apply positive_4step_ind; try discriminate. - destruct p0. + destruct p0. * intros; repeat split; auto with chains. * intros; repeat split; auto with chains. * compute; repeat split;auto; try discriminate. + destruct p0. * intros; repeat split; auto with chains. * intros; repeat split; auto with chains. * compute; repeat split;auto; try discriminate. + compute; intuition auto; discriminate. Qed.
imports: Coq(Arith NArith)