proposition: Lemma dicho_gt : forall p:positive, 3 < p -> 1 < dicho p.
proof: Proof. intros p H; unfold dicho; generalize (dicho_aux_lt p H). intro H0; assert (2 <= N.pos p / (N.pos (dicho_aux p)) )%N. - replace 2%N with (2%N * Npos (dicho_aux p) / Npos (dicho_aux p))%N. + apply N.div_le_mono; try discriminate. * replace 2%N with (Npos 2%positive); cbn;auto. + rewrite N.div_mul; [auto | discriminate]. - case_eq (N.pos p / N.pos (dicho_aux p))%N. + intro H2; rewrite H2 in H1; destruct H1. reflexivity. + intros p0 H2; rewrite H2 in H1. assert (1 < N.pos p0)%N. * apply N.lt_le_trans with 2%N;auto. reflexivity. * assumption. Qed.
imports: Coq(Arith NArith)