proposition: Theorem ofnat_S_gt_0 : forall n : nat, 0 < [Datatypes.S n].
proof: Proof. unfold ofnat. intros n; induction n as [| n IH]; simpl in *. - apply lt_succ_diag_r. - apply lt_trans with (S 0). + apply lt_succ_diag_r. + now rewrite <- succ_lt_mono. Qed.
imports: NumPrelude NZAxioms NZBase NZOrder NZAddOrder PeanoNat