proposition: Lemma ltzlt : forall x y : Z, (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Z.abs_nat x < Z.abs_nat y.
proof: Proof. intros. change (Z.abs_nat y > Z.abs_nat x) in |- *. apply gtzgt. assumption. assumption. apply Z.lt_gt. assumption. Qed.
imports: ZArith EqNat lemmas