proposition: Theorem mult_id_le_inv : forall n m : nat, n * n <= m * m -> n <= m.
proof: Proof. intros n m H; case (Nat.le_gt_cases n m); auto; intros H1; contradict H; apply Nat.lt_nge. apply Nat.le_lt_trans with (n * m); auto with arith. apply le_mult; auto with arith; apply Nat.lt_le_incl; auto. apply mult_lt_bis; auto with arith; apply Nat.le_lt_trans with (2 := H1); auto with arith. Qed.
imports: Coq(Arith ArithRing)