proposition: Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m.
proof: Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). - apply lt_le_incl; now apply lt_le_trans with 0. - destruct (le_gt_cases n m) as [LE|LT]; trivial. apply square_lt_mono_nonneg in LT; order. Qed.
imports: NZAxioms NZAddOrder