proposition: Lemma SF_sup_ly (f : R -> R) (a b : R) (n : nat) : SF_ly (SF_sup_seq f a b n) = behead (pairmap (Sup_fct f) 0 (unif_part a b n)).
proof: Proof. by apply SF_ly_f2. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy