proposition: Lemma mult_lt_r_elim : forall x x' y, x * y < x' * y -> x < x'.
proof: Proof. induction x; induction y; simpl; nia. Qed.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)