proposition: Lemma leif_pM x1 x2 y1 y2 C1 C2 : 0 <= x1 -> 0 <= x2 -> x1 <= y1 ?= iff C1 -> x2 <= y2 ?= iff C2 -> x1 * x2 <= y1 * y2 ?= iff (y1 * y2 == 0) || C1 && C2.
proof: Proof. move=> x1_ge0 x2_ge0 le_xy1 le_xy2; have [y_0 | ] := eqVneq _ 0. apply/leifP; rewrite y_0 /= mulf_eq0 !eq_le x1_ge0 x2_ge0 !andbT. move/eqP: y_0; rewrite mulf_eq0. by case/pred2P=> <-; rewrite (le_xy1, le_xy2) ?orbT. rewrite /= mulf_eq0 => /norP[y1nz y2nz]. have y1_gt0: 0 < y1 by rewrite lt_def y1nz (le_trans _ le_xy1). have [x2_0 | x2nz] := eqVneq x2 0. apply/leifP; rewrite -le_xy2 x2_0 eq_sym (negPf y2nz) andbF mulr0. by rewrite mulr_gt0 // lt_def y2nz -x2_0 le_xy2. have:= le_xy2; rewrite -(mono_leif (ler_pM2l y1_gt0)). by apply: leif_trans; rewrite (mono_leif (ler_pM2r _)) // lt_def x2nz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)