proposition: Lemma Rmult_0_lt_compat : forall a, a < 0 -> 0 < a * a.
proof: Proof. intros a a_neg ; apply Rlt_le_trans with ((- a) * (- a)) ; [| right ; ring] ; apply Rmult_lt_0_compat ; lra. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq