proposition: Lemma SF_inf_subdiv_val (f : R -> R) (a b : R) (n : nat) : subdivision_val (SF_inf_r f a b n) = match (Rle_dec a b) with | left _ => behead (pairmap (fun x y => real (Inf_fct f x y)) 0 (unif_part a b n)) | right _ => behead (pairmap (fun x y => real (Inf_fct f x y)) 0 (unif_part b a n)) end.
proof: Proof. rewrite /SF_inf_r ; case: (Rle_dec a b) => Hab //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy