proposition: Lemma StepFun_P3 : forall a b c:R, a <= b -> adapted_couple (fct_cte c) a b (cons a (cons b nil)) (cons c nil).
proof: Proof. intros; unfold adapted_couple; repeat split. - unfold ordered_Rlist; intros; simpl in H0; inversion H0; [ simpl; assumption | elim (Nat.nle_succ_0 _ H2) ]. - simpl; unfold Rmin; decide (Rle_dec a b) with H; reflexivity. - simpl; unfold Rmax; decide (Rle_dec a b) with H; reflexivity. - unfold constant_D_eq, open_interval; intros; simpl in H0; inversion H0; [ reflexivity | elim (Nat.nle_succ_0 _ H3) ]. Qed.
imports: Rbase Rfunctions Ranalysis_reg Classical_Prop List RList Lia Lra