proposition: Lemma sqrt_up_le_lin : forall a, 0<=a -> √°a<=a.
proof: Proof. intros a Ha. le_elim Ha. - rewrite sqrt_up_eqn; trivial. apply le_succ_l. apply le_lt_trans with (P a). + apply sqrt_le_lin. now rewrite <- lt_succ_r, (lt_succ_pred 0). + rewrite <- (lt_succ_pred 0 a) at 2; trivial. apply lt_succ_diag_r. - now rewrite <- Ha, sqrt_up_0. Qed.
imports: NZAxioms NZMulOrder