proposition: Theorem sqr_inv : forall n m : nat, m * m <= n -> n < S m * S m -> sqr n = m.
proof: Proof. intros n m H1 H2. case (proj1 (Nat.lt_eq_cases 0 m)); auto with arith; intros H3. cut (m <= n); [ intros H4 | idtac ]. unfold sqr in |- *; generalize (max_such_prop (fun x : nat => x * x <= n) (fun x : nat => le_dec1 (x * x) n) n); case (max_such (fun x : nat => x * x <= n) (fun x : nat => le_dec1 (x * x) n) n). intros H5; case H5. exists m; auto with arith. intros H6 (H7, H8); case (H8 m); auto with arith. intros n0 H. case H; auto with arith. exists m; auto with arith. intros H5 (H6, H7). case (proj1 (Nat.lt_eq_cases (S n0) m)); auto with arith. apply Nat.lt_succ_r; apply mult_id_lt_inv. apply Nat.le_lt_trans with (1 := H6); auto with arith. intros H0; case (H7 m); auto with arith. apply Nat.le_trans with (2 := H1); auto with arith. apply Nat.le_trans with (m * 1); auto with arith. rewrite Nat.mul_1_r; auto with arith. rewrite <- H3; rewrite <- H3 in H2; simpl in H2; inversion H2. simpl in |- *; auto. inversion H0. Qed.
imports: Coq(Arith ArithRing)