proposition: Theorem mult_id_lt_inv : forall n m : nat, n * n < m * m -> n < m.
proof: Proof. intros n m H; case (Nat.le_gt_cases m n); auto; intros H1; contradict H; apply Nat.le_ngt. apply Nat.le_trans with (n * m); auto with arith. apply le_mult; auto with arith. Qed.
imports: Coq(Arith ArithRing)