proposition: Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b.
proof: Proof. intros a b (LEb,LTb). assert (Ha : 0<=a) by (transitivity (b²); trivial using square_nonneg). assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order). assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). assert (b <= √a). - apply lt_succ_r, square_lt_simpl_nonneg; [|order]. now apply lt_le_incl, lt_succ_r. - assert (√a <= b). + apply lt_succ_r, square_lt_simpl_nonneg; [|order]. now apply lt_le_incl, lt_succ_r. + order. Qed.
imports: NZAxioms NZMulOrder