proposition: Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
proof: Proof. intros a Ha. destruct (le_gt_cases a 0) as [H|H]. - setoid_replace a with 0 by order. now rewrite sqrt_0. - destruct (le_gt_cases a 1) as [H'|H']. + rewrite <- le_succ_l, <- one_succ in H. setoid_replace a with 1 by order. now rewrite sqrt_1. + now apply lt_le_incl, sqrt_lt_lin. Qed.
imports: NZAxioms NZMulOrder