proposition: Lemma sqrt_pred_square : forall a, 0<a -> √(P a²) == P a.
proof: Proof. intros a Ha. apply sqrt_unique. assert (EQ := lt_succ_pred 0 a Ha). rewrite EQ. split. - apply lt_succ_r. rewrite (lt_succ_pred 0). + assert (0 <= P a) by (now rewrite <- lt_succ_r, EQ). assert (P a < a) by (now rewrite <- le_succ_l, EQ). apply mul_lt_mono_nonneg; trivial. + now apply mul_pos_pos. - apply le_succ_l. rewrite (lt_succ_pred 0). + reflexivity. + now apply mul_pos_pos. Qed.
imports: NZAxioms NZMulOrder