proposition: Lemma StepFun_P20 : forall (l:list R) (f:R -> R), (0 < length l)%nat -> length l = S (length (FF l f)).
proof: Proof. intros l f H; induction l; [ elim (Nat.lt_irrefl _ H) | simpl; rewrite RList_P18; rewrite RList_P14; reflexivity ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra