proposition: Lemma estimate_absCC : forall x : CC, {X : IR | [0] [<] X | AbsCC x [<=] X}.
proof: Proof. intros. exists (AbsCC x[+][1]). astepl ([0][+]ZeroR). apply plus_resp_leEq_less. apply AbsCC_nonneg. apply pos_one. astepl (AbsCC x[+][0]). apply less_leEq. apply plus_resp_less_lft. apply pos_one. Qed.
imports: CoRN.fta.CC_Props