proposition: Lemma SubEqui_P9 : forall (a b:R) (del:posreal) (f:R -> R) (h:a < b), { g:StepFun a b | g b = f b /\ (forall i:nat, (i < pred (length (SubEqui del h)))%nat -> constant_D_eq g (co_interval (pos_Rl (SubEqui del h) i) (pos_Rl (SubEqui del h) (S i))) (f (pos_Rl (SubEqui del h) i))) }.
proof: Proof. intros; apply StepFun_P38; [ apply SubEqui_P7 | apply SubEqui_P1 | apply SubEqui_P2 ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra