proposition: Lemma sqrt_up_lt_lin : forall a, 2<a -> √°a < a.
proof: Proof. intros a Ha. rewrite sqrt_up_eqn by order'. assert (Ha' := lt_succ_pred 2 a Ha). rewrite <- Ha' at 2. rewrite <- succ_lt_mono. apply sqrt_lt_lin. rewrite succ_lt_mono. now rewrite Ha', <- two_succ. Qed.
imports: NZAxioms NZMulOrder