proposition: Theorem max_div_prop3 : forall n : nat, 1 < n -> max_div n < n.
proof: Proof. intros n; case n. intros H1; inversion H1. intros n1; case n1. simpl in |- *; auto with arith. 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 H1; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)