proposition: Theorem sqr_le : forall n : nat, sqr n * sqr n <= n.
proof: Proof. intros n; unfold sqr in |- *; generalize (max_such_prop (fun x => x * x <= n) (fun x => le_dec1 (x * x) n) n); case (max_such (fun x => x * x <= n) (fun x => le_dec1 (x * x) n)). simpl in |- *; intros H1; case H1; auto with arith. exists 0; split; auto with arith. intros n0 H; case H; auto with arith. exists 0; split; auto with arith. intros H2 (H3, H4); auto. Qed.
imports: Coq(Arith ArithRing)