proposition: Lemma StepFun_P5 : forall (a b:R) (f:R -> R) (l:list R), is_subdivision f a b l -> is_subdivision f b a l.
proof: Proof. destruct 1 as (x,(H0,(H1,(H2,(H3,H4))))); exists x; repeat split; try assumption. - rewrite H1; apply Rmin_comm. - rewrite H2; apply Rmax_comm. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra