proposition: Lemma mult_lt_compat_lr : forall i j k l, i <= j -> j > 0 -> k < l -> i * k < j * l.
proof: Proof. intros. case (bigN_le_gt_dec j i); intro. assert (i==j). apply BigN.le_antisymm; hyp. rewrite H2. rewrite <- (BigN.mul_lt_mono_pos_l _ _ _ H0). hyp. apply BigN.mul_lt_mono; hyp. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)