proposition: Lemma nexp_resp_pos : forall (x : R) k, [0] [<] x -> [0] [<] x[^]k.
proof: Proof. intros. elim k. simpl in |- *. apply pos_one. intros. simpl in |- *. apply mult_resp_pos. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)