proposition: Theorem square_le_mono : forall n m, n <= m <-> n * n <= m * m.
proof: Proof. intros n m; split; intro; [apply square_le_mono_nonneg | apply square_le_simpl_nonneg]; try assumption; apply le_0_l. Qed.
imports: NAddOrder