proposition: Theorem square_lt_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). - now apply lt_le_trans with 0. - destruct (lt_ge_cases n m) as [LT|LE]; trivial. apply square_le_mono_nonneg in LE; order. Qed.
imports: NZAxioms NZAddOrder