proposition: Lemma Kneser_1'' : q [<] [1].
proof: Proof. unfold q in |- *. apply shift_minus_less'. rstepl ([0][+]OneR). apply plus_resp_less_rht. unfold Smallest, Small, Smaller in |- *. apply mult_resp_pos; apply p3m_pos. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma