proposition: Lemma Kneser_1' : Half [<=] q.
proof: Proof. unfold q in |- *. apply shift_leEq_minus. astepl (Smallest[+]Half). apply shift_plus_leEq. unfold Half in |- *. rstepr ([1] [/]TwoNZ:IR). unfold Smallest, Small, Smaller in |- *. generalize (p3m_smaller n gt_n_0). intro Hn. generalize (p3m_smaller (two_n * n)). intro H2nn. apply leEq_transitive with (Half[*] (Half:IR)). apply mult_resp_leEq_both; auto. apply less_leEq; apply p3m_pos. apply less_leEq; apply p3m_pos. apply H2nn. unfold two_n in |- *. elim gt_n_0. auto with arith. intros. simpl in |- *. auto with arith. rstepr ([1] [/]TwoNZ[*]OneR). apply less_leEq. apply mult_resp_less_lft. exact (half_lt1 _). exact (pos_half _). Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma