proposition: Lemma b_0'_exists : forall eta : IR, [0] [<] eta -> {b_0' : CC | AbsCC (b_0'[-]b_0) [<=] eta | b_0' [#] [0]}.
proof: Proof. intros. exact (Cexis_AFS_CC [0] b_0 eta X). Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma