proposition: Lemma dicho_lt : forall p:positive, 3 < p -> dicho p < p.
proof: Proof. intros p H; unfold dicho; generalize (dicho_aux_gt p H); intro H0. generalize (N.div_lt (N.pos p) (N.pos (dicho_aux p))); intro H1. unfold N2pos; case_eq (N.pos p / N.pos (dicho_aux p))%N. - intro; transitivity 3%positive ;[reflexivity | auto]. - intros p0 H2; assert (N.pos p0 < N.pos p)%N. + rewrite <- H2; now apply H1. + assumption. Qed.
imports: Coq(Arith NArith)