proposition: Lemma sqrt_spec_nonneg : forall b, b² < (S b)² -> 0 <= b.
proof: Proof. intros b LT. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. exfalso. assert ((S b)² < b²). - rewrite mul_succ_l, <- (add_0_r b²). apply add_lt_le_mono. + apply mul_lt_mono_neg_l; trivial. apply lt_succ_diag_r. + now apply le_succ_l. - order. Qed.
imports: NZAxioms NZMulOrder