proposition: Lemma strictly_monotonous_in_monotonous_in : forall D f, strictly_monotonous_in D f -> monotonous_in D f.
proof: Proof. intros D f [Hd | Hi] ; [left ; apply strictly_decreasing_in_decreasing_in | right ; apply strictly_increasing_in_increasing_in] ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra