proposition: Lemma eta_0_pos : [0] [<] eta_0.
proof: Proof. unfold eta_0 in |- *. apply pos_div_two. apply pos_div_four. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma