proposition: Lemma maps_translation : forall y, maps_compacts_into realline realline (FId{+} [-C-]y).
proof: Proof. intros y a b Hab H. exists (a[+]y); exists (b[+]y[+][1]). cut (a[+]y [<] b[+]y[+][1]). intro H0. exists H0. split. split. intros x Hx H1; simpl in |- *; inversion_clear H1; split. apply plus_resp_leEq; auto. apply less_leEq; apply leEq_less_trans with (b[+]y). apply plus_resp_leEq; auto. apply less_plusOne. apply leEq_less_trans with (b[+]y). apply plus_resp_leEq; auto. apply less_plusOne. Qed.
imports: CoRN.transc.TaylorSeries Coq(Lia)