x : x <> 0 <-> 0 < x. Proof. split. - destruct (nat_0_or_pos x); auto. intros E;destruct E;trivial. - intros E1 E2. rewrite E2 in E1. destruct (irreflexivity (<) 0). trivial. Qed.
Require Import Require Import Require Import