proposition: Theorem sqr_lt : forall n : nat, n < S (sqr n) * S (sqr 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)). case n; auto with arith. intros n0 H; case H; auto with arith. exists 0; split; auto with arith. intros H2 (H3, H4); auto. apply not_le_lt; auto with arith. intros n0 H; case H; auto with arith. exists 0; split; auto with arith. intros H2 (H3, H4); auto. apply not_le_lt; auto with arith. case ((proj1 (Nat.lt_eq_cases _ _)) H2); intros H5. apply H4; auto with arith. rewrite H5; auto with arith. apply Nat.lt_nge; auto with arith. apply Nat.lt_le_trans with (S n); auto with arith. pattern (S n) at 1 in |- *; replace (S n) with (S n * 1); auto with arith. Qed.
imports: Coq(Arith ArithRing)