proposition: Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²).
proof: Proof. intros a Ha. split. - intros H. exists √a. split. + apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. now rewrite sqrt_square, sqrt_up_square. Qed.
imports: NZAxioms NZMulOrder