proposition: Lemma ltAddRhs : forall (a b : IR), [0][<]b -> a[<]a[+]b.
proof: Proof. intros ? ? Hlt. pose proof (leEq_reflexive _ a) as Hr. apply (plus_resp_less_leEq _ _ _ _ _ Hlt) in Hr. eapply less_wdl in Hr;[|apply cm_lft_unit_unfolded]. eapply less_wdr;[| apply cag_commutes_unfolded]. trivial. Qed.
imports: CoRN.ftc.FTC Coq.setoid_ring.Ring CoRN.tactics.CornTac CoRN.algebra.CRing_as_Ring CoRN.ftc.Derivative CoRN.ftc.Integral