[STATEMENT]
lemma comp_injective_below_complement:
  "injective y \<Longrightarrow> -x * y \<le> -(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. injective y \<Longrightarrow> - x * y \<le> - (x * y)
[PROOF STEP]
by (metis p_antitone_iff comp_associative comp_right_isotone comp_right_one schroeder_4_p)