proposition: Theorem max_div_prop2 : forall n p : nat, max_div n < p -> p < n -> ~ divides p n.
proof: Proof. intros n; case n. intros p H1 H2; inversion H2. intros n1; case n1. intros p H1 H2; inversion H2. red in |- *; intros (x, H3). rewrite Nat.mul_comm in H3; discriminate. inversion H0. intros n2; unfold max_div in |- *; case (max_such_prop (fun x : nat => divides x (S (S n2))) (fun x : nat => divides1_dec x (S (S n2))) (S n2)); auto. exists 1; split; auto with arith. intros H (H0, H'0) p H1 H2; apply H'0; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)