proposition: Lemma nat_ge_0 : forall n : nat, (Z_of_nat n >= 0)%Z.
proof: Proof. simple induction n. simpl in |- *. unfold Z.ge in |- *. simpl in |- *. discriminate. intros m IHm. change (Z_of_nat (S m) >= Z_of_nat 0)%Z in |- *. apply Znat.inj_ge. unfold ge in |- *. apply le_O_n. Qed.
imports: ZArith EqNat lemmas