proposition: Lemma leif_nM x1 x2 y1 y2 C1 C2 : y1 <= 0 -> y2 <= 0 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> y1 * y2 <= x1 * x2 ?= iff (x1 * x2 == 0) || C1 && C2.
proof: Proof. rewrite -!oppr_ge0 -mulrNN -[x1 * x2]mulrNN => y1le0 y2le0 le_xy1 le_xy2. by apply: leif_pM => //; rewrite (nmono_leif lerN2). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)