proposition: Lemma val_positive: forall a, zero < a -> nf a -> forall N, (0 < val (S (S N)) a)%nat.
proof: Proof. induction a. inversion 1. simpl. intros. replace 0 with (0 + 0)%nat. apply plus_lt_le_compat. 2:auto with arith. 2: simpl;auto. replace 0 with (0 * 0)%nat. apply Lt.le_lt_trans with (0 * n)%nat. simpl;auto. simpl. generalize (val (S (S N1)) a1). induction n0. simpl. auto with arith. simpl. replace 0 with (0 * (S n))%nat. apply mult_lt_compat_r. replace 0 with (0 + 0)%nat. apply plus_lt_le_compat. apply power_positive. auto with arith. simpl;auto. auto with arith. simpl;auto. simpl;auto. Qed.
imports: More_nat Arith ArithRing EPSILON0