proposition: Lemma sqrt_up_pos : forall a, 0 < √°a <-> 0 < a.
proof: Proof. intros a. split; intros Ha. - apply sqrt_up_lt_cancel. now rewrite sqrt_up_0. - rewrite <- le_succ_l, <- one_succ, <- sqrt_up_1. apply sqrt_up_le_mono. now rewrite one_succ, le_succ_l. Qed.
imports: NZAxioms NZMulOrder