proposition: Theorem lt_Zlt_inv : forall n m : nat, (Z_of_nat n < Z_of_nat m)%Z -> n < m.
proof: Proof. intros n m H'; case (Nat.le_gt_cases n m); auto. intros H'0. case (proj1 (Nat.lt_eq_cases _ _) H'0); auto with zarith. intros H'1. contradict H'. apply Zle_not_lt; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz