proposition: Lemma sqrt_up_square : forall a, 0<=a -> √°(a²) == a.
proof: Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn by (now apply mul_pos_pos). rewrite sqrt_pred_square; trivial. apply (lt_succ_pred 0); trivial. - rewrite sqrt_up_eqn0; trivial. rewrite <- Ha. now nzsimpl. Qed.
imports: NZAxioms NZMulOrder