proposition: Lemma strictly_increasing_in_injective_in : forall D f, strictly_increasing_in D f -> injective_in D f.
proof: Proof. intros D f f_inc x y x_in y_in feq ; destruct (Rtotal_order x y) as [Hlt | [Heq | Hgt]]. destruct (Rlt_irrefl (f y)) ; apply Rle_lt_trans with (f x). rewrite feq ; reflexivity. apply f_inc ; assumption. assumption. destruct (Rlt_irrefl (f x)) ; apply Rle_lt_trans with (f y). rewrite feq ; reflexivity. apply f_inc ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Rfunction_facts Ranalysis_def Ranalysis_def_simpl MyRIneq MyR_dist Lra