x y : 1 < x -> 1 ≤ y -> 1 < x * y. Proof. intros. apply lt_le_trans with x; trivial. apply ge_1_mult_le_compat_r;[trivial| |apply reflexivity]. transitivity 1. - apply le_0_1. - apply lt_le;trivial. Qed.
Require Import