proposition: Lemma Rpow_2_inf_0 : forall x, (x^2 < 0 -> False)%R.
proof: Proof. intros. replace (x ^ 2)%R with (Rsqr x) in * by (unfold Rsqr ; simpl ; ring). assert (Rsqr x >= 0) by (auto with real). lra. Qed.
imports: Complex Cpow_plus