proposition: Lemma Rle_neq_Rlt : forall a b, a <= b -> a <> b -> a < b.
proof: Proof. intros a b a_le a_neq ; destruct (Rlt_le_dec a b) ; [| destruct a_neq ; apply Rle_antisym] ; assumption. Qed.
imports: Rbase AltSeries Rseries_def Rtrigo_facts Ratan Cpow_plus Complex Lra MyRIneq