proposition: Lemma SF_val_subdiv_val (f : R -> R) (a b : R) (n : nat) : subdivision_val (sf_SF_val_fun f a b n) = match (Rle_dec a b) with | left _ => SF_val_ly f a b n | right _ => SF_val_ly f b a n end.
proof: Proof. rewrite /sf_SF_val_fun ; case: (Rle_dec a b) => Hab //. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy