proposition: Lemma sqrt_up_unique : forall a b, 0<b -> (P b)² < a <= b² -> √°a == b.
proof: Proof. intros a b Hb (LEb,LTb). assert (Ha : 0<a) by (apply le_lt_trans with (P b)²; trivial using square_nonneg). rewrite sqrt_up_eqn; trivial. assert (Hb' := lt_succ_pred 0 b Hb). rewrite <- Hb'. f_equiv. apply sqrt_unique. rewrite <- le_succ_l, <- lt_succ_r, Hb'. rewrite (lt_succ_pred 0 a Ha). now split. Qed.
imports: NZAxioms NZMulOrder