proposition: Theorem max_div_prop1 : forall n : nat, divides (max_div n) n.
proof: Proof. intros n; case n. exists 0; ring. intros n1; case n1. exists 1; simpl; ring. 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. Qed.
imports: Coq(Arith ArithRing Wf_nat) Bertrand(Div)