proposition: Lemma strictly_increasing_increasing f : strictly_increasing f -> increasing f.
proof: Proof. apply strictly_increasing_in_increasing_in. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra