proposition: Lemma sqr_pos_lt : forall a, a <> 0 -> 0 < a * a.
proof: Proof. intros a a_neq ; destruct (Rlt_le_dec a 0). apply Rmult_0_lt_compat ; assumption. apply Rmult_lt_0_compat ; apply Rle_neq_Rlt ; (assumption || symmetry ; assumption). Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq