proposition: Lemma ltMinusRhs: forall (x y: IR), [0] [<]y -> x[-]y[<]x.
proof: Proof. intros. apply shift_minus_less. apply ltAddRhs; auto. Qed.
imports: CoRN.ftc.FTC Coq.setoid_ring.Ring CoRN.tactics.CornTac CoRN.algebra.CRing_as_Ring CoRN.ftc.Derivative CoRN.ftc.Integral