proposition: Theorem sqr_mono : forall n m : nat, n <= m -> sqr n <= sqr m.
proof: Proof. intros n m H; elim H; auto with arith. intros m0 H0 H1. apply Nat.le_trans with (1 := H1). apply Nat.lt_succ_r; apply mult_id_lt_inv. apply Nat.le_lt_trans with m0. apply sqr_le; auto. apply Nat.lt_trans with (S m0); auto with arith; apply sqr_lt; auto. Qed.
imports: Coq(Arith ArithRing)