proposition: Lemma cpoly_CC_contin : forall (x : CC) (e : IR), [0] [<] e -> {d : IR | [0] [<] d | forall x', AbsCC (x[-]x') [<=] d -> AbsCC (g ! x[-]g ! x') [<=] e}.
proof: Proof. elim g. intros. exists OneR. intros. apply pos_one. intros. apply leEq_wdl with ZeroR. apply less_leEq. auto. cut ([0] [=] AbsCC ([0][-][0])). auto. Step_final (AbsCC [0]). intros a f. intro H. do 2 intro. intro H0. elim (mult_CC_contin x f ! x e H0). intro d1. intros H1 H2. elim H2. clear H2. intro c. intros H2 H3. elim (H x c H2). clear H. intro d2. intros H H4. exists (Min d1 d2). apply less_Min; auto. intros. simpl in |- *. cut (AbsCC (a[+]x[*]f ! x[-](a[+]x'[*]f ! x')) [<=] e). auto. apply leEq_wdl with (AbsCC (x[*]f ! x[-]x'[*]f ! x')). apply H3. clear H3. apply leEq_transitive with (Min d1 d2); auto. apply Min_leEq_lft. apply H4. clear H4. apply leEq_transitive with (Min d1 d2); auto. apply Min_leEq_rht. apply AbsCC_wd. rational. Qed.
imports: CoRN.fta.CC_Props