proposition: Lemma strictly_decreasing_in_decreasing_in : forall D f, strictly_decreasing_in D f -> decreasing_in D f.
proof: Proof. intros D f f_decr x y Dx Dy [Hlt | Heq]. left ; apply f_decr ; assumption. subst ; reflexivity. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra